diff --git a/Src/PChecker/CheckerCore/Actors/Exceptions/OnEventDroppedHandler.cs b/Src/PChecker/CheckerCore/Actors/Exceptions/OnEventDroppedHandler.cs
deleted file mode 100644
index a96ad02dc..000000000
--- a/Src/PChecker/CheckerCore/Actors/Exceptions/OnEventDroppedHandler.cs
+++ /dev/null
@@ -1,12 +0,0 @@
-// Copyright (c) Microsoft Corporation.
-// Licensed under the MIT License.
-
-using PChecker.Actors.Events;
-
-namespace PChecker.Actors.Exceptions
-{
-    /// <summary>
-    /// Handles the <see cref="IActorRuntime.OnEventDropped"/> event.
-    /// </summary>
-    public delegate void OnEventDroppedHandler(Event e, ActorId target);
-}
\ No newline at end of file
diff --git a/Src/PChecker/CheckerCore/Actors/IActorRuntime.cs b/Src/PChecker/CheckerCore/Actors/IActorRuntime.cs
deleted file mode 100644
index c93bb2909..000000000
--- a/Src/PChecker/CheckerCore/Actors/IActorRuntime.cs
+++ /dev/null
@@ -1,158 +0,0 @@
-// Copyright (c) Microsoft Corporation.
-// Licensed under the MIT License.
-
-using System;
-using System.Threading.Tasks;
-using PChecker.Actors.Events;
-using PChecker.Actors.Exceptions;
-using PChecker.Actors.Logging;
-using PChecker.Runtime;
-
-namespace PChecker.Actors
-{
-    /// <summary>
-    /// Interface that exposes runtime methods for creating and executing actors.
-    /// </summary>
-    public interface IActorRuntime : ICoyoteRuntime
-    {
-        /// <summary>
-        /// Callback that is fired when an event is dropped.
-        /// </summary>
-        event OnEventDroppedHandler OnEventDropped;
-
-        /// <summary>
-        /// Creates a fresh actor id that has not yet been bound to any actor.
-        /// </summary>
-        /// <param name="type">Type of the actor.</param>
-        /// <param name="name">Optional name used for logging.</param>
-        /// <returns>The result is the actor id.</returns>
-        ActorId CreateActorId(Type type, string name = null);
-
-        /// <summary>
-        /// Creates a actor id that is uniquely tied to the specified unique name. The
-        /// returned actor id can either be a fresh id (not yet bound to any actor), or
-        /// it can be bound to a previously created actor. In the second case, this actor
-        /// id can be directly used to communicate with the corresponding actor.
-        /// </summary>
-        /// <param name="type">Type of the actor.</param>
-        /// <param name="name">Unique name used to create or get the actor id.</param>
-        /// <returns>The result is the actor id.</returns>
-        ActorId CreateActorIdFromName(Type type, string name);
-
-        /// <summary>
-        /// Creates a new actor of the specified <see cref="Type"/> and with the specified
-        /// optional <see cref="Event"/>. This event can only be used to access its payload,
-        /// and cannot be handled.
-        /// </summary>
-        /// <param name="type">Type of the actor.</param>
-        /// <param name="initialEvent">Optional event used during initialization.</param>
-        /// <param name="opGroupId">Optional id that can be used to identify this operation.</param>
-        /// <returns>The result is the actor id.</returns>
-        ActorId CreateActor(Type type, Event initialEvent = null, Guid opGroupId = default);
-
-        /// <summary>
-        /// Creates a new actor of the specified <see cref="Type"/> and name, and with the
-        /// specified optional <see cref="Event"/>. This event can only be used to access
-        /// its payload, and cannot be handled.
-        /// </summary>
-        /// <param name="type">Type of the actor.</param>
-        /// <param name="name">Optional name used for logging.</param>
-        /// <param name="initialEvent">Optional event used during initialization.</param>
-        /// <param name="opGroupId">Optional id that can be used to identify this operation.</param>
-        /// <returns>The result is the actor id.</returns>
-        ActorId CreateActor(Type type, string name, Event initialEvent = null, Guid opGroupId = default);
-
-        /// <summary>
-        /// Creates a new actor of the specified type, using the specified <see cref="ActorId"/>.
-        /// This method optionally passes an <see cref="Event"/> to the new actor, which can only
-        /// be used to access its payload, and cannot be handled.
-        /// </summary>
-        /// <param name="id">Unbound actor id.</param>
-        /// <param name="type">Type of the actor.</param>
-        /// <param name="initialEvent">Optional event used during initialization.</param>
-        /// <param name="opGroupId">Optional id that can be used to identify this operation.</param>
-        /// <returns>The result is the actor id.</returns>
-        ActorId CreateActor(ActorId id, Type type, Event initialEvent = null, Guid opGroupId = default);
-
-        /// <summary>
-        /// Creates a new actor of the specified <see cref="Type"/> and with the specified
-        /// optional <see cref="Event"/>. This event can only be used to access its payload,
-        /// and cannot be handled. The method returns only when the actor is initialized and
-        /// the <see cref="Event"/> (if any) is handled.
-        /// </summary>
-        /// <param name="type">Type of the actor.</param>
-        /// <param name="initialEvent">Optional event used during initialization.</param>
-        /// <param name="opGroupId">Optional id that can be used to identify this operation.</param>
-        /// <returns>Task that represents the asynchronous operation. The task result is the actor id.</returns>
-        Task<ActorId> CreateActorAndExecuteAsync(Type type, Event initialEvent = null, Guid opGroupId = default);
-
-        /// <summary>
-        /// Creates a new actor of the specified <see cref="Type"/> and name, and with the
-        /// specified optional <see cref="Event"/>. This event can only be used to access
-        /// its payload, and cannot be handled. The method returns only when the actor is
-        /// initialized and the <see cref="Event"/> (if any) is handled.
-        /// </summary>
-        /// <param name="type">Type of the actor.</param>
-        /// <param name="name">Optional name used for logging.</param>
-        /// <param name="initialEvent">Optional event used during initialization.</param>
-        /// <param name="opGroupId">Optional id that can be used to identify this operation.</param>
-        /// <returns>Task that represents the asynchronous operation. The task result is the actor id.</returns>
-        Task<ActorId> CreateActorAndExecuteAsync(Type type, string name, Event initialEvent = null,
-            Guid opGroupId = default);
-
-        /// <summary>
-        /// Creates a new actor of the specified <see cref="Type"/>, using the specified unbound
-        /// actor id, and passes the specified optional <see cref="Event"/>. This event can only
-        /// be used to access its payload, and cannot be handled. The method returns only when
-        /// the actor is initialized and the <see cref="Event"/> (if any)
-        /// is handled.
-        /// </summary>
-        /// <param name="id">Unbound actor id.</param>
-        /// <param name="type">Type of the actor.</param>
-        /// <param name="initialEvent">Optional event used during initialization.</param>
-        /// <param name="opGroupId">Optional id that can be used to identify this operation.</param>
-        /// <returns>Task that represents the asynchronous operation. The task result is the actor id.</returns>
-        Task<ActorId> CreateActorAndExecuteAsync(ActorId id, Type type, Event initialEvent = null,
-            Guid opGroupId = default);
-
-        /// <summary>
-        /// Sends an asynchronous <see cref="Event"/> to an actor.
-        /// </summary>
-        /// <param name="targetId">The id of the target.</param>
-        /// <param name="e">The event to send.</param>
-        /// <param name="opGroupId">Optional id that can be used to identify this operation.</param>
-        void SendEvent(ActorId targetId, Event e, Guid opGroupId = default);
-
-        /// <summary>
-        /// Sends an <see cref="Event"/> to an actor. Returns immediately if the target was already
-        /// running. Otherwise blocks until the target handles the event and reaches quiescense.
-        /// </summary>
-        /// <param name="targetId">The id of the target.</param>
-        /// <param name="e">The event to send.</param>
-        /// <param name="opGroupId">Optional id that can be used to identify this operation.</param>
-        /// <returns>Task that represents the asynchronous operation. The task result is true if
-        /// the event was handled, false if the event was only enqueued.</returns>
-        Task<bool> SendEventAndExecuteAsync(ActorId targetId, Event e, Guid opGroupId = default);
-
-        /// <summary>
-        /// Returns the operation group id of the actor with the specified id. Returns <see cref="Guid.Empty"/>
-        /// if the id is not set, or if the <see cref="ActorId"/> is not associated with this runtime. During
-        /// testing, the runtime asserts that the specified actor is currently executing.
-        /// </summary>
-        /// <param name="currentActorId">The id of the currently executing actor.</param>
-        /// <returns>The unique identifier.</returns>
-        Guid GetCurrentOperationGroupId(ActorId currentActorId);
-
-        /// <summary>
-        /// Use this method to register an <see cref="IActorRuntimeLog"/>.
-        /// </summary>
-        /// <param name="log">The log writer to register.</param>
-        void RegisterLog(IActorRuntimeLog log);
-
-        /// <summary>
-        /// Use this method to unregister a previously registered <see cref="IActorRuntimeLog"/>.
-        /// </summary>
-        /// <param name="log">The previously registered log writer to unregister.</param>
-        void RemoveLog(IActorRuntimeLog log);
-    }
-}
\ No newline at end of file
diff --git a/Src/PChecker/CheckerCore/CheckerConfiguration.cs b/Src/PChecker/CheckerCore/CheckerConfiguration.cs
index 04ddade0c..e7bf83b15 100644
--- a/Src/PChecker/CheckerCore/CheckerConfiguration.cs
+++ b/Src/PChecker/CheckerCore/CheckerConfiguration.cs
@@ -236,7 +236,7 @@ public int MaxSchedulingSteps
         /// This is the AssemblyQualifiedName of the type to load.
         /// </summary>
         [DataMember]
-        public string CustomActorRuntimeLogType;
+        public string CustomStateMachineRuntimeLogType;
 
         /// <summary>
         /// Enables debugging.
diff --git a/Src/PChecker/CheckerCore/Coverage/ActivityCoverageReporter.cs b/Src/PChecker/CheckerCore/Coverage/ActivityCoverageReporter.cs
index e0b29a15c..9a3b2f1d4 100644
--- a/Src/PChecker/CheckerCore/Coverage/ActivityCoverageReporter.cs
+++ b/Src/PChecker/CheckerCore/Coverage/ActivityCoverageReporter.cs
@@ -5,7 +5,7 @@
 using System.Collections.Generic;
 using System.IO;
 using System.Linq;
-using PChecker.Actors.Events;
+using PChecker.StateMachines.Events;
 
 namespace PChecker.Coverage
 {
diff --git a/Src/PChecker/CheckerCore/Coverage/ActorRuntimeLogEventCoverage.cs b/Src/PChecker/CheckerCore/Coverage/StateMachineRuntimeLogEventCoverage.cs
similarity index 66%
rename from Src/PChecker/CheckerCore/Coverage/ActorRuntimeLogEventCoverage.cs
rename to Src/PChecker/CheckerCore/Coverage/StateMachineRuntimeLogEventCoverage.cs
index 8d1385701..f9185b17c 100644
--- a/Src/PChecker/CheckerCore/Coverage/ActorRuntimeLogEventCoverage.cs
+++ b/Src/PChecker/CheckerCore/Coverage/StateMachineRuntimeLogEventCoverage.cs
@@ -4,28 +4,28 @@
 using System;
 using System.Collections.Generic;
 using System.Runtime.Serialization;
-using PChecker.Actors;
-using PChecker.Actors.Events;
-using PChecker.Actors.Logging;
+using PChecker.StateMachines;
+using PChecker.StateMachines.Events;
+using PChecker.StateMachines.Logging;
 
 namespace PChecker.Coverage
 {
     /// <summary>
-    /// This class maintains information about events received and sent from each state of each actor.
+    /// This class maintains information about events received and sent from each state of each state machine.
     /// </summary>
     [DataContract]
     public class EventCoverage
     {
         /// <summary>
-        /// Map from states to the list of events received by that state.  The state id is fully qualified by
-        /// the actor id it belongs to.
+        /// Map from states to the list of events received by that state. The state id is fully qualified by
+        /// the state machine id it belongs to.
         /// </summary>
         [DataMember]
         private readonly Dictionary<string, HashSet<string>> EventsReceived = new Dictionary<string, HashSet<string>>();
 
         /// <summary>
         /// Map from states to the list of events sent by that state.  The state id is fully qualified by
-        /// the actor id it belongs to.
+        /// the state machine id it belongs to.
         /// </summary>
         [DataMember]
         private readonly Dictionary<string, HashSet<string>> EventsSent = new Dictionary<string, HashSet<string>>();
@@ -44,7 +44,7 @@ internal void AddEventReceived(string stateId, string eventId)
         /// <summary>
         /// Get list of events received by the given fully qualified state.
         /// </summary>
-        /// <param name="stateId">The actor qualified state name</param>
+        /// <param name="stateId">The state machine qualified state name</param>
         public IEnumerable<string> GetEventsReceived(string stateId)
         {
             if (EventsReceived.TryGetValue(stateId, out var set))
@@ -69,7 +69,7 @@ internal void AddEventSent(string stateId, string eventId)
         /// <summary>
         /// Get list of events sent by the given state.
         /// </summary>
-        /// <param name="stateId">The actor qualified state name</param>
+        /// <param name="stateId">The state machine qualified state name</param>
         public IEnumerable<string> GetEventsSent(string stateId)
         {
             if (EventsSent.TryGetValue(stateId, out var set))
@@ -102,12 +102,12 @@ private static void MergeHashSets(Dictionary<string, HashSet<string>> ours, Dict
         }
     }
 
-    internal class ActorRuntimeLogEventCoverage : IActorRuntimeLog
+    internal class StateMachineRuntimeLogEventCoverage : IStateMachineRuntimeLog
     {
         private readonly EventCoverage InternalEventCoverage = new EventCoverage();
         private Event Dequeued;
 
-        public ActorRuntimeLogEventCoverage()
+        public StateMachineRuntimeLogEventCoverage()
         {
         }
 
@@ -121,11 +121,7 @@ public void OnCompleted()
         {
         }
 
-        public void OnCreateActor(ActorId id, string creatorName, string creatorType)
-        {
-        }
-
-        public void OnCreateStateMachine(ActorId id, string creatorName, string creatorType)
+        public void OnCreateStateMachine(StateMachineId id, string creatorName, string creatorType)
         {
         }
 
@@ -133,34 +129,34 @@ public void OnCreateMonitor(string monitorType)
         {
         }
 
-        public void OnDefaultEventHandler(ActorId id, string stateName)
+        public void OnDefaultEventHandler(StateMachineId id, string stateName)
         {
             Dequeued = DefaultEvent.Instance;
         }
 
-        public void OnDequeueEvent(ActorId id, string stateName, Event e)
+        public void OnDequeueEvent(StateMachineId id, string stateName, Event e)
         {
             Dequeued = e;
         }
 
-        public void OnEnqueueEvent(ActorId id, Event e)
+        public void OnEnqueueEvent(StateMachineId id, Event e)
         {
         }
 
-        public void OnExceptionHandled(ActorId id, string stateName, string actionName, Exception ex)
+        public void OnExceptionHandled(StateMachineId id, string stateName, string actionName, Exception ex)
         {
         }
 
-        public void OnExceptionThrown(ActorId id, string stateName, string actionName, Exception ex)
+        public void OnExceptionThrown(StateMachineId id, string stateName, string actionName, Exception ex)
         {
         }
 
-        public void OnExecuteAction(ActorId id, string handlingStateName, string currentStateName, string actionName)
+        public void OnExecuteAction(StateMachineId id, string handlingStateName, string currentStateName, string actionName)
         {
             OnEventHandled(id, handlingStateName);
         }
 
-        private void OnEventHandled(ActorId id, string stateName)
+        private void OnEventHandled(StateMachineId id, string stateName)
         {
             if (Dequeued != null)
             {
@@ -169,16 +165,16 @@ private void OnEventHandled(ActorId id, string stateName)
             }
         }
 
-        public void OnGotoState(ActorId id, string currentStateName, string newStateName)
+        public void OnGotoState(StateMachineId id, string currentStateName, string newStateName)
         {
             OnEventHandled(id, currentStateName);
         }
 
-        public void OnHalt(ActorId id, int inboxSize)
+        public void OnHalt(StateMachineId id, int inboxSize)
         {
         }
 
-        public void OnHandleRaisedEvent(ActorId id, string stateName, Event e)
+        public void OnHandleRaisedEvent(StateMachineId id, string stateName, Event e)
         {
             Dequeued = e;
         }
@@ -211,39 +207,39 @@ public void OnRandom(object result, string callerName, string callerType)
         {
         }
 
-        public void OnPopState(ActorId id, string currentStateName, string restoredStateName)
+        public void OnPopState(StateMachineId id, string currentStateName, string restoredStateName)
         {
         }
 
-        public void OnPopStateUnhandledEvent(ActorId id, string stateName, Event e)
+        public void OnPopStateUnhandledEvent(StateMachineId id, string stateName, Event e)
         {
         }
 
-        public void OnPushState(ActorId id, string currentStateName, string newStateName)
+        public void OnPushState(StateMachineId id, string currentStateName, string newStateName)
         {
             OnEventHandled(id, currentStateName);
         }
 
-        public void OnRaiseEvent(ActorId id, string stateName, Event e)
+        public void OnRaiseEvent(StateMachineId id, string stateName, Event e)
         {
             var eventName = e.GetType().FullName;
             EventCoverage.AddEventSent(GetStateId(id.Type, stateName), eventName);
         }
 
-        public void OnReceiveEvent(ActorId id, string stateName, Event e, bool wasBlocked)
+        public void OnReceiveEvent(StateMachineId id, string stateName, Event e, bool wasBlocked)
         {
             var eventName = e.GetType().FullName;
             EventCoverage.AddEventReceived(GetStateId(id.Type, stateName), eventName);
         }
 
-        public void OnSendEvent(ActorId targetActorId, string senderName, string senderType, string senderStateName,
+        public void OnSendEvent(StateMachineId targetStateMachineId, string senderName, string senderType, string senderStateName,
             Event e, Guid opGroupId, bool isTargetHalted)
         {
             var eventName = e.GetType().FullName;
             EventCoverage.AddEventSent(GetStateId(senderType, senderStateName), eventName);
         }
 
-        public void OnStateTransition(ActorId id, string stateName, bool isEntry)
+        public void OnStateTransition(StateMachineId id, string stateName, bool isEntry)
         {
         }
 
@@ -251,20 +247,20 @@ public void OnStrategyDescription(string strategyName, string description)
         {
         }
 
-        public void OnWaitEvent(ActorId id, string stateName, Type eventType)
+        public void OnWaitEvent(StateMachineId id, string stateName, Type eventType)
         {
         }
 
-        public void OnWaitEvent(ActorId id, string stateName, params Type[] eventTypes)
+        public void OnWaitEvent(StateMachineId id, string stateName, params Type[] eventTypes)
         {
         }
 
-        private static string GetStateId(string actorType, string stateName)
+        private static string GetStateId(string stateMachineType, string stateName)
         {
-            var id = ResolveActorTypeName(actorType);
+            var id = ResolvestateMachineTypeName(stateMachineType);
             if (string.IsNullOrEmpty(stateName))
             {
-                if (actorType == null)
+                if (stateMachineType == null)
                 {
                     stateName = "ExternalState";
                 }
@@ -277,35 +273,22 @@ private static string GetStateId(string actorType, string stateName)
             return id += "." + stateName;
         }
 
-        private static string ResolveActorTypeName(string actorType)
+        private static string ResolvestateMachineTypeName(string stateMachineType)
         {
-            if (actorType == null)
+            if (stateMachineType == null)
             {
-                // The sender id can be null if an event is fired from non-actor code.
+                // The sender id can be null if an event is fired from non-stateMachine code.
                 return "ExternalCode";
             }
 
-            return actorType;
+            return stateMachineType;
         }
 
-        private static string GetLabel(string actorId, string fullyQualifiedName)
+        private static string GetLabel(string stateMachineId, string fullyQualifiedName)
         {
-            if (fullyQualifiedName == null)
-            {
-                // then this is probably an Actor, not a StateMachine.  For Actors we can invent a state
-                // name equal to the short name of the class, this then looks like a Constructor which is fine.
-                var pos = actorId.LastIndexOf(".");
-                if (pos > 0)
-                {
-                    return actorId.Substring(pos + 1);
-                }
-
-                return actorId;
-            }
-
-            if (fullyQualifiedName.StartsWith(actorId))
+            if (fullyQualifiedName.StartsWith(stateMachineId))
             {
-                fullyQualifiedName = fullyQualifiedName.Substring(actorId.Length + 1).Trim('+');
+                fullyQualifiedName = fullyQualifiedName.Substring(stateMachineId.Length + 1).Trim('+');
             }
 
             return fullyQualifiedName;
diff --git a/Src/PChecker/CheckerCore/Coverage/ActorRuntimeLogGraphBuilder.cs b/Src/PChecker/CheckerCore/Coverage/StateMachineRuntimeLogGraphBuilder.cs
similarity index 90%
rename from Src/PChecker/CheckerCore/Coverage/ActorRuntimeLogGraphBuilder.cs
rename to Src/PChecker/CheckerCore/Coverage/StateMachineRuntimeLogGraphBuilder.cs
index 752570a51..610998bee 100644
--- a/Src/PChecker/CheckerCore/Coverage/ActorRuntimeLogGraphBuilder.cs
+++ b/Src/PChecker/CheckerCore/Coverage/StateMachineRuntimeLogGraphBuilder.cs
@@ -7,26 +7,25 @@
 using System.Runtime.Serialization;
 using System.Text;
 using System.Xml.Linq;
-using PChecker.Actors;
-using PChecker.Actors.Events;
-using PChecker.Actors.Logging;
+using PChecker.StateMachines;
+using PChecker.StateMachines.Events;
+using PChecker.StateMachines.Logging;
 
 namespace PChecker.Coverage
 {
     /// <summary>
-    /// Implements the <see cref="IActorRuntimeLog"/> and builds a directed graph
+    /// Implements the <see cref="IStateMachineRuntimeLog"/> and builds a directed graph
     /// from the recorded events and state transitions.
     /// </summary>
-    public class ActorRuntimeLogGraphBuilder : IActorRuntimeLog
+    public class StateMachineRuntimeLogGraphBuilder : IStateMachineRuntimeLog
     {
         private Graph CurrentGraph;
-        private readonly Dictionary<ActorId, EventInfo> Dequeued = new Dictionary<ActorId, EventInfo>(); // current dequeued event.
-        private readonly Dictionary<ActorId, string> HaltedStates = new Dictionary<ActorId, string>(); // halted state for given actor.
+        private readonly Dictionary<StateMachineId, EventInfo> Dequeued = new Dictionary<StateMachineId, EventInfo>(); // current dequeued event.
+        private readonly Dictionary<StateMachineId, string> HaltedStates = new Dictionary<StateMachineId, string>(); // halted state for given state machine.
         private readonly bool MergeEventLinks; // merge events from node A to node B instead of making them separate links.
         private const string ExternalCodeName = "ExternalCode";
         private const string ExternalStateName = "ExternalState";
         private const string StateMachineCategory = "StateMachine";
-        private const string ActorCategory = "Actor";
         private const string MonitorCategory = "Monitor";
 
         private class EventInfo
@@ -51,7 +50,7 @@ private class PopStateEvent : Event
         {
         }
 
-        static ActorRuntimeLogGraphBuilder()
+        static StateMachineRuntimeLogGraphBuilder()
         {
             EventAliases[typeof(GotoStateEvent).FullName] = "goto";
             EventAliases[typeof(HaltEvent).FullName] = "halt";
@@ -63,9 +62,9 @@ static ActorRuntimeLogGraphBuilder()
         }
 
         /// <summary>
-        /// Initializes a new instance of the <see cref="ActorRuntimeLogGraphBuilder"/> class.
+        /// Initializes a new instance of the <see cref="StateMachineRuntimeLogGraphBuilder"/> class.
         /// </summary>
-        public ActorRuntimeLogGraphBuilder(bool mergeEventLinks)
+        public StateMachineRuntimeLogGraphBuilder(bool mergeEventLinks)
         {
             MergeEventLinks = mergeEventLinks;
             CurrentGraph = new Graph();
@@ -102,37 +101,26 @@ public Graph Graph
         }
 
         /// <inheritdoc/>
-        public void OnCreateActor(ActorId id, string creatorName, string creatorType)
+        public void OnCreateStateMachine(StateMachineId id, string creatorName, string creatorType)
         {
             lock (Inbox)
             {
-                var resolvedId = GetResolveActorId(id?.Name, id?.Type);
-                var node = Graph.GetOrCreateNode(resolvedId);
-                node.Category = ActorCategory;
-            }
-        }
-
-        /// <inheritdoc/>
-        public void OnCreateStateMachine(ActorId id, string creatorName, string creatorType)
-        {
-            lock (Inbox)
-            {
-                var resolvedId = GetResolveActorId(id?.Name, id?.Type);
+                var resolvedId = GetResolveStateMachineId(id?.Name, id?.Type);
                 var node = Graph.GetOrCreateNode(resolvedId);
                 node.Category = StateMachineCategory;
             }
         }
 
         /// <inheritdoc/>
-        public void OnSendEvent(ActorId targetActorId, string senderName, string senderType, string senderStateName,
+        public void OnSendEvent(StateMachineId targetStateMachineId, string senderName, string senderType, string senderStateName,
             Event e, Guid opGroupId, bool isTargetHalted)
         {
             var eventName = e.GetType().FullName;
-            AddEvent(targetActorId.Name, targetActorId.Type, senderName, senderType, senderStateName, eventName);
+            AddEvent(targetStateMachineId.Name, targetStateMachineId.Type, senderName, senderType, senderStateName, eventName);
         }
 
         /// <inheritdoc/>
-        public void OnRaiseEvent(ActorId id, string stateName, Event e)
+        public void OnRaiseEvent(StateMachineId id, string stateName, Event e)
         {
             var eventName = e.GetType().FullName;
             // Raising event to self.
@@ -140,16 +128,16 @@ public void OnRaiseEvent(ActorId id, string stateName, Event e)
         }
 
         /// <inheritdoc/>
-        public void OnEnqueueEvent(ActorId id, Event e)
+        public void OnEnqueueEvent(StateMachineId id, Event e)
         {
         }
 
         /// <inheritdoc/>
-        public void OnDequeueEvent(ActorId id, string stateName, Event e)
+        public void OnDequeueEvent(StateMachineId id, string stateName, Event e)
         {
             lock (Inbox)
             {
-                var resolvedId = GetResolveActorId(id?.Name, id?.Type);
+                var resolvedId = GetResolveStateMachineId(id?.Name, id?.Type);
                 var eventName = e.GetType().FullName;
                 var info = PopEvent(resolvedId, eventName);
                 if (info != null)
@@ -181,9 +169,9 @@ private EventInfo PopEvent(string resolvedId, string eventName)
         }
 
         /// <inheritdoc/>
-        public void OnReceiveEvent(ActorId id, string stateName, Event e, bool wasBlocked)
+        public void OnReceiveEvent(StateMachineId id, string stateName, Event e, bool wasBlocked)
         {
-            var resolvedId = GetResolveActorId(id?.Name, id?.Type);
+            var resolvedId = GetResolveStateMachineId(id?.Name, id?.Type);
             lock (Inbox)
             {
                 if (Inbox.TryGetValue(resolvedId, out var inbox))
@@ -195,7 +183,7 @@ public void OnReceiveEvent(ActorId id, string stateName, Event e, bool wasBlocke
                         if (info.Event == eventName)
                         {
                             // Yay, found it so we can draw the complete link connecting the Sender state to this state!
-                            var category = string.IsNullOrEmpty(stateName) ? ActorCategory : StateMachineCategory;
+                            var category = StateMachineCategory;
                             var source = GetOrCreateChild(info.Name, info.Type, info.State);
                             var target = GetOrCreateChild(id?.Name, id?.Type, category, stateName);
                             GetOrCreateEventLink(source, target, info);
@@ -208,17 +196,17 @@ public void OnReceiveEvent(ActorId id, string stateName, Event e, bool wasBlocke
         }
 
         /// <inheritdoc/>
-        public void OnWaitEvent(ActorId id, string stateName, Type eventType)
+        public void OnWaitEvent(StateMachineId id, string stateName, Type eventType)
         {
         }
 
         /// <inheritdoc/>
-        public void OnWaitEvent(ActorId id, string stateName, params Type[] eventTypes)
+        public void OnWaitEvent(StateMachineId id, string stateName, params Type[] eventTypes)
         {
         }
 
         /// <inheritdoc/>
-        public void OnStateTransition(ActorId id, string stateName, bool isEntry)
+        public void OnStateTransition(StateMachineId id, string stateName, bool isEntry)
         {
             if (isEntry)
             {
@@ -228,19 +216,19 @@ public void OnStateTransition(ActorId id, string stateName, bool isEntry)
         }
 
         /// <inheritdoc/>
-        public void OnExecuteAction(ActorId id, string handlingStateName, string currentStateName, string actionName)
+        public void OnExecuteAction(StateMachineId id, string handlingStateName, string currentStateName, string actionName)
         {
             LinkTransition(typeof(DoActionEvent), id, handlingStateName, currentStateName, null);
         }
 
         /// <inheritdoc/>
-        public void OnGotoState(ActorId id, string currentStateName, string newStateName)
+        public void OnGotoState(StateMachineId id, string currentStateName, string newStateName)
         {
             LinkTransition(typeof(GotoStateEvent), id, currentStateName, currentStateName, newStateName);
         }
 
         /// <inheritdoc/>
-        public void OnHalt(ActorId id, int inboxSize)
+        public void OnHalt(StateMachineId id, int inboxSize)
         {
             lock (Inbox)
             {
@@ -268,11 +256,11 @@ public void OnHalt(ActorId id, int inboxSize)
         }
 
         /// <inheritdoc/>
-        public void OnDefaultEventHandler(ActorId id, string stateName)
+        public void OnDefaultEventHandler(StateMachineId id, string stateName)
         {
             lock (Inbox)
             {
-                var resolvedId = GetResolveActorId(id?.Name, id?.Type);
+                var resolvedId = GetResolveStateMachineId(id?.Name, id?.Type);
                 var eventName = typeof(DefaultEvent).FullName;
                 AddEvent(id.Name, id.Type, id.Name, id.Type, stateName, eventName);
                 Dequeued[id] = PopEvent(resolvedId, eventName);
@@ -280,13 +268,13 @@ public void OnDefaultEventHandler(ActorId id, string stateName)
         }
 
         /// <inheritdoc/>
-        public void OnHandleRaisedEvent(ActorId id, string stateName, Event e)
+        public void OnHandleRaisedEvent(StateMachineId id, string stateName, Event e)
         {
             lock (Inbox)
             {
                 // We used the inbox to store raised event, but it should be the first one handled since
                 // raised events are highest priority.
-                var resolvedId = GetResolveActorId(id?.Name, id?.Type);
+                var resolvedId = GetResolveStateMachineId(id?.Name, id?.Type);
                 lock (Inbox)
                 {
                     if (Inbox.TryGetValue(resolvedId, out var inbox))
@@ -307,21 +295,21 @@ public void OnHandleRaisedEvent(ActorId id, string stateName, Event e)
         }
 
         /// <inheritdoc/>
-        public void OnPopStateUnhandledEvent(ActorId actorId, string currentStateName, Event e)
+        public void OnPopStateUnhandledEvent(StateMachineId stateMachineId, string currentStateName, Event e)
         {
             if (e is HaltEvent)
             {
-                HaltedStates[actorId] = currentStateName;
+                HaltedStates[stateMachineId] = currentStateName;
             }
         }
 
         /// <inheritdoc/>
-        public void OnExceptionThrown(ActorId id, string stateName, string actionName, Exception ex)
+        public void OnExceptionThrown(StateMachineId id, string stateName, string actionName, Exception ex)
         {
         }
 
         /// <inheritdoc/>
-        public void OnExceptionHandled(ActorId id, string stateName, string actionName, Exception ex)
+        public void OnExceptionHandled(StateMachineId id, string stateName, string actionName, Exception ex)
         {
         }
 
@@ -460,11 +448,11 @@ public Graph SnapshotGraph(bool reset)
             return result;
         }
 
-        private string GetResolveActorId(string name, string type)
+        private string GetResolveStateMachineId(string name, string type)
         {
             if (type == null)
             {
-                // The sender id can be null if an event is fired from non-actor code.
+                // The sender id can be null if an event is fired from non-stateMachine code.
                 return ExternalCodeName;
             }
 
@@ -479,7 +467,7 @@ private string GetResolveActorId(string name, string type)
         private EventInfo AddEvent(string targetName, string targetType, string senderName, string senderType,
             string senderStateName, string eventName)
         {
-            var targetId = GetResolveActorId(targetName, targetType);
+            var targetId = GetResolveStateMachineId(targetName, targetType);
             EventInfo info = null;
             lock (Inbox)
             {
@@ -503,7 +491,7 @@ private EventInfo AddEvent(string targetName, string targetType, string senderNa
             return info;
         }
 
-        private void LinkTransition(Type transitionType, ActorId id, string handlingStateName,
+        private void LinkTransition(Type transitionType, StateMachineId id, string handlingStateName,
             string currentStateName, string newStateName)
         {
             var name = id.Name;
@@ -548,10 +536,10 @@ private GraphNode GetOrCreateChild(string name, string type, string stateName, s
 
                 var initalStateName = stateName;
 
-                // make label relative to fully qualified actor id (it's usually a nested class).
+                // make label relative to fully qualified state machine id (it's usually a nested class).
                 stateName = GetLabel(name, type, stateName);
 
-                var id = GetResolveActorId(name, type);
+                var id = GetResolveStateMachineId(name, type);
                 var parent = Graph.GetOrCreateNode(id);
                 parent.AddAttribute("Group", "Expanded");
 
@@ -626,13 +614,7 @@ private string GetLabel(string name, string type, string fullyQualifiedName)
             }
 
             AddNamespace(type);
-            if (string.IsNullOrEmpty(fullyQualifiedName))
-            {
-                // then this is probably an Actor, not a StateMachine.  For Actors we can invent a state
-                // name equal to the short name of the class, this then looks like a Constructor which is fine.
-                fullyQualifiedName = CollapseMachineInstances ? type : name;
-            }
-
+            
             var len = fullyQualifiedName.Length;
             var index = fullyQualifiedName.LastIndexOfAny(TypeSeparators);
             if (index > 0)
@@ -908,8 +890,8 @@ public void WriteDgml(TextWriter writer, bool includeDefaultStyles)
       <Condition Expression=""HasCategory('Error')"" />
       <Setter Property=""Background"" Value=""#FFC15656"" />
     </Style>
-    <Style TargetType=""Node"" GroupLabel=""Actor"" ValueLabel=""True"">
-      <Condition Expression=""HasCategory('Actor')"" />
+    <Style TargetType=""Node"" GroupLabel=""StateMachine"" ValueLabel=""True"">
+      <Condition Expression=""HasCategory('StateMachine')"" />
       <Setter Property=""Background"" Value=""#FF57AC56"" />
     </Style>
     <Style TargetType=""Node"" GroupLabel=""Monitor"" ValueLabel=""True"">
diff --git a/Src/PChecker/CheckerCore/PRuntime/GodMachine.cs b/Src/PChecker/CheckerCore/PRuntime/GodMachine.cs
index a629d66cd..603e6d386 100644
--- a/Src/PChecker/CheckerCore/PRuntime/GodMachine.cs
+++ b/Src/PChecker/CheckerCore/PRuntime/GodMachine.cs
@@ -1,6 +1,6 @@
 using System;
-using PChecker.Actors;
-using PChecker.Actors.Events;
+using PChecker.StateMachines;
+using PChecker.StateMachines.Events;
 
 namespace PChecker.PRuntime
 {
@@ -9,7 +9,7 @@ public class _GodMachine : StateMachine
         private void InitOnEntry(Event e)
         {
             var mainMachine = (e as Config).MainMachine;
-            CreateActor(mainMachine, mainMachine.Name,
+            CreateStateMachine(mainMachine, mainMachine.Name,
                 new PMachine.InitializeParametersEvent(
                     new PMachine.InitializeParameters("I_" + mainMachine.Name, null)));
         }
diff --git a/Src/PChecker/CheckerCore/PRuntime/PEvent.cs b/Src/PChecker/CheckerCore/PRuntime/PEvent.cs
index 33af7d679..23a16cc4d 100644
--- a/Src/PChecker/CheckerCore/PRuntime/PEvent.cs
+++ b/Src/PChecker/CheckerCore/PRuntime/PEvent.cs
@@ -1,5 +1,5 @@
 using System;
-using PChecker.Actors.Events;
+using PChecker.StateMachines.Events;
 using PChecker.PRuntime.Values;
 
 namespace PChecker.PRuntime
diff --git a/Src/PChecker/CheckerCore/PRuntime/PJsonFormatter.cs b/Src/PChecker/CheckerCore/PRuntime/PJsonFormatter.cs
index 1ab95ee70..250d43cf0 100644
--- a/Src/PChecker/CheckerCore/PRuntime/PJsonFormatter.cs
+++ b/Src/PChecker/CheckerCore/PRuntime/PJsonFormatter.cs
@@ -4,15 +4,15 @@
 using System;
 using System.Linq;
 using System.Threading.Tasks;
-using PChecker.Actors;
-using PChecker.Actors.Events;
-using PChecker.Actors.Logging;
+using PChecker.StateMachines;
+using PChecker.StateMachines.Events;
+using PChecker.StateMachines.Logging;
 using PChecker.PRuntime.Exceptions;
 
 namespace PChecker.PRuntime
 {
     /// <summary>
-    /// This class implements IActorRuntimeLog and generates log output in an XML format.
+    /// This class implements IStateMachineRuntimeLog and generates log output in an XML format.
     /// </summary>
     public class PJsonFormatter : PCheckerLogJsonFormatter
     {
@@ -98,27 +98,9 @@ public override void OnAssertionFailure(string error)
             Writer.AddLog(error);
             Writer.AddToLogs();
         }
-
-        public override void OnCreateActor(ActorId id, string creatorName, string creatorType)
-        {
-            if (id.Name.Contains("GodMachine") || creatorName.Contains("GodMachine"))
-            {
-                return;
-            }
-
-            var source = creatorName ?? $"task '{Task.CurrentId}'";
-            var log = $"{id} was created by {source}.";
-
-            Writer.AddLogType(JsonWriter.LogType.CreateActor);
-            Writer.LogDetails.Id = id.ToString();
-            Writer.LogDetails.CreatorName = source;
-            Writer.LogDetails.CreatorType = creatorType;
-            Writer.AddLog(log);
-            Writer.AddToLogs(updateVcMap: true);
-        }
-
+        
         /// <inheritdoc/>
-        public override void OnCreateStateMachine(ActorId id, string creatorName, string creatorType)
+        public override void OnCreateStateMachine(StateMachineId id, string creatorName, string creatorType)
         {
             if (id.Name.Contains("GodMachine") || creatorName.Contains("GodMachine"))
             {
@@ -136,7 +118,7 @@ public override void OnCreateStateMachine(ActorId id, string creatorName, string
             Writer.AddToLogs(updateVcMap: true);
         }
 
-        public override void OnDefaultEventHandler(ActorId id, string stateName)
+        public override void OnDefaultEventHandler(StateMachineId id, string stateName)
         {
             stateName = GetShortName(stateName);
 
@@ -151,7 +133,7 @@ public override void OnDefaultEventHandler(ActorId id, string stateName)
             Writer.AddToLogs(updateVcMap: true);
         }
 
-        public override void OnDequeueEvent(ActorId id, string stateName, Event e)
+        public override void OnDequeueEvent(StateMachineId id, string stateName, Event e)
         {
             if (stateName.Contains("__InitState__") || id.Name.Contains("GodMachine"))
             {
@@ -172,11 +154,11 @@ public override void OnDequeueEvent(ActorId id, string stateName, Event e)
             Writer.AddToLogs(updateVcMap: true);
         }
 
-        public override void OnEnqueueEvent(ActorId id, Event e)
+        public override void OnEnqueueEvent(StateMachineId id, Event e)
         {
         }
 
-        public override void OnExceptionHandled(ActorId id, string stateName, string actionName, Exception ex)
+        public override void OnExceptionHandled(StateMachineId id, string stateName, string actionName, Exception ex)
         {
             if (ex is PNonStandardReturnException)
             {
@@ -196,7 +178,7 @@ public override void OnExceptionHandled(ActorId id, string stateName, string act
             Writer.AddToLogs(updateVcMap: true);
         }
 
-        public override void OnExceptionThrown(ActorId id, string stateName, string actionName, Exception ex)
+        public override void OnExceptionThrown(StateMachineId id, string stateName, string actionName, Exception ex)
         {
             if (ex is PNonStandardReturnException)
             {
@@ -216,11 +198,11 @@ public override void OnExceptionThrown(ActorId id, string stateName, string acti
             Writer.AddToLogs(updateVcMap: true);
         }
 
-        public override void OnExecuteAction(ActorId id, string handlingStateName, string currentStateName, string actionName)
+        public override void OnExecuteAction(StateMachineId id, string handlingStateName, string currentStateName, string actionName)
         {
         }
 
-        public override void OnGotoState(ActorId id, string currentStateName, string newStateName)
+        public override void OnGotoState(StateMachineId id, string currentStateName, string newStateName)
         {
             if (currentStateName.Contains("__InitState__") || id.Name.Contains("GodMachine"))
             {
@@ -241,7 +223,7 @@ public override void OnGotoState(ActorId id, string currentStateName, string new
             Writer.AddToLogs(updateVcMap: true);
         }
 
-        public override void OnHalt(ActorId id, int inboxSize)
+        public override void OnHalt(StateMachineId id, int inboxSize)
         {
             var log = $"{id} halted with {inboxSize} events in its inbox.";
 
@@ -252,11 +234,11 @@ public override void OnHalt(ActorId id, int inboxSize)
             Writer.AddToLogs(updateVcMap: true);
         }
 
-        public override void OnHandleRaisedEvent(ActorId id, string stateName, Event e)
+        public override void OnHandleRaisedEvent(StateMachineId id, string stateName, Event e)
         {
         }
 
-        public override void OnPopState(ActorId id, string currentStateName, string restoredStateName)
+        public override void OnPopState(StateMachineId id, string currentStateName, string restoredStateName)
         {
             currentStateName = string.IsNullOrEmpty(currentStateName) ? "[not recorded]" : currentStateName;
             var reenteredStateName = restoredStateName ?? string.Empty;
@@ -270,7 +252,7 @@ public override void OnPopState(ActorId id, string currentStateName, string rest
             Writer.AddToLogs(updateVcMap: true);
         }
 
-        public override void OnPopStateUnhandledEvent(ActorId id, string stateName, Event e)
+        public override void OnPopStateUnhandledEvent(StateMachineId id, string stateName, Event e)
         {
             var log = $"{id} popped state {stateName} due to unhandled event '{e.GetType().Name}'.";
 
@@ -282,7 +264,7 @@ public override void OnPopStateUnhandledEvent(ActorId id, string stateName, Even
             Writer.AddToLogs(updateVcMap: true);
         }
 
-        public override void OnPushState(ActorId id, string currentStateName, string newStateName)
+        public override void OnPushState(StateMachineId id, string currentStateName, string newStateName)
         {
             var log = $"{id} pushed from state '{currentStateName}' to state '{newStateName}'.";
 
@@ -294,7 +276,7 @@ public override void OnPushState(ActorId id, string currentStateName, string new
             Writer.AddToLogs(updateVcMap: true);
         }
 
-        public override void OnRaiseEvent(ActorId id, string stateName, Event e)
+        public override void OnRaiseEvent(StateMachineId id, string stateName, Event e)
         {
             stateName = GetShortName(stateName);
             string eventName = GetEventNameWithPayload(e);
@@ -318,7 +300,7 @@ public override void OnRaiseEvent(ActorId id, string stateName, Event e)
             Writer.AddToLogs(updateVcMap: true);
         }
 
-        public override void OnReceiveEvent(ActorId id, string stateName, Event e, bool wasBlocked)
+        public override void OnReceiveEvent(StateMachineId id, string stateName, Event e, bool wasBlocked)
         {
             stateName = GetShortName(stateName);
             string eventName = GetEventNameWithPayload(e);
@@ -337,7 +319,7 @@ public override void OnReceiveEvent(ActorId id, string stateName, Event e, bool
             Writer.AddToLogs(updateVcMap: true);
         }
 
-        public override void OnSendEvent(ActorId targetActorId, string senderName, string senderType, string senderStateName,
+        public override void OnSendEvent(StateMachineId targetStateMachineId, string senderName, string senderType, string senderStateName,
             Event e, Guid opGroupId, bool isTargetHalted)
         {
             senderStateName = GetShortName(senderStateName);
@@ -347,13 +329,13 @@ public override void OnSendEvent(ActorId targetActorId, string senderName, strin
             var sender = !string.IsNullOrEmpty(senderName)
                 ? $"'{senderName}' in state '{senderStateName}'"
                 : $"The runtime";
-            var log = $"{sender} sent event '{eventName}' to '{targetActorId}'{isHalted}{opGroupIdMsg}.";
+            var log = $"{sender} sent event '{eventName}' to '{targetStateMachineId}'{isHalted}{opGroupIdMsg}.";
 
             Writer.AddLogType(JsonWriter.LogType.SendEvent);
             Writer.LogDetails.Sender = !string.IsNullOrEmpty(senderName) ? senderName : "Runtime";
             Writer.LogDetails.State = senderStateName;
             Writer.LogDetails.Event = GetShortName(e.GetType().Name);
-            Writer.LogDetails.Target = targetActorId.ToString();
+            Writer.LogDetails.Target = targetStateMachineId.ToString();
             Writer.LogDetails.OpGroupId = opGroupId.ToString();
             Writer.LogDetails.IsTargetHalted = isTargetHalted;
             Writer.LogDetails.Payload = GetEventPayloadInJson(e);
@@ -361,7 +343,7 @@ public override void OnSendEvent(ActorId targetActorId, string senderName, strin
             Writer.AddToLogs(updateVcMap: true);
         }
 
-        public override void OnStateTransition(ActorId id, string stateName, bool isEntry)
+        public override void OnStateTransition(StateMachineId id, string stateName, bool isEntry)
         {
             if (stateName.Contains("__InitState__") || id.Name.Contains("GodMachine"))
             {
@@ -380,7 +362,7 @@ public override void OnStateTransition(ActorId id, string stateName, bool isEntr
             Writer.AddToLogs(updateVcMap: true);
         }
 
-        public override void OnWaitEvent(ActorId id, string stateName, Type eventType)
+        public override void OnWaitEvent(StateMachineId id, string stateName, Type eventType)
         {
             stateName = GetShortName(stateName);
 
@@ -396,7 +378,7 @@ public override void OnWaitEvent(ActorId id, string stateName, Type eventType)
             Writer.AddToLogs(updateVcMap: true);
         }
 
-        public override void OnWaitEvent(ActorId id, string stateName, params Type[] eventTypes)
+        public override void OnWaitEvent(StateMachineId id, string stateName, params Type[] eventTypes)
         {
             stateName = GetShortName(stateName);
             string eventNames;
diff --git a/Src/PChecker/CheckerCore/PRuntime/PLogFormatter.cs b/Src/PChecker/CheckerCore/PRuntime/PLogFormatter.cs
index 151ef1c1d..1364f178b 100644
--- a/Src/PChecker/CheckerCore/PRuntime/PLogFormatter.cs
+++ b/Src/PChecker/CheckerCore/PRuntime/PLogFormatter.cs
@@ -1,8 +1,8 @@
 using System;
 using System.Linq;
-using PChecker.Actors;
-using PChecker.Actors.Events;
-using PChecker.Actors.Logging;
+using PChecker.StateMachines;
+using PChecker.StateMachines.Events;
+using PChecker.StateMachines.Logging;
 using PChecker.PRuntime.Exceptions;
 
 namespace PChecker.PRuntime
@@ -33,7 +33,7 @@ private string GetEventNameWithPayload(Event e)
             return $"{GetShortName(e.GetType().Name)}{msg}";
         }
 
-        public override void OnStateTransition(ActorId id, string stateName, bool isEntry)
+        public override void OnStateTransition(StateMachineId id, string stateName, bool isEntry)
         {
             if (stateName.Contains("__InitState__") || id.Name.Contains("GodMachine"))
             {
@@ -43,22 +43,22 @@ public override void OnStateTransition(ActorId id, string stateName, bool isEntr
             base.OnStateTransition(id, GetShortName(stateName), isEntry);
         }
 
-        public override void OnPopStateUnhandledEvent(ActorId id, string stateName, Event e)
+        public override void OnPopStateUnhandledEvent(StateMachineId id, string stateName, Event e)
         {
             base.OnPopStateUnhandledEvent(id, GetShortName(stateName), e);
         }
 
-        public override void OnDefaultEventHandler(ActorId id, string stateName)
+        public override void OnDefaultEventHandler(StateMachineId id, string stateName)
         {
             base.OnDefaultEventHandler(id, GetShortName(stateName));
         }
 
-        public override void OnWaitEvent(ActorId id, string stateName, params Type[] eventTypes)
+        public override void OnWaitEvent(StateMachineId id, string stateName, params Type[] eventTypes)
         {
             base.OnWaitEvent(id, GetShortName(stateName), eventTypes);
         }
 
-        public override void OnWaitEvent(ActorId id, string stateName, Type eventType)
+        public override void OnWaitEvent(StateMachineId id, string stateName, Type eventType)
         {
             base.OnWaitEvent(id, GetShortName(stateName), eventType);
         }
@@ -72,17 +72,7 @@ public override void OnMonitorStateTransition(string monitorType, string stateNa
 
             base.OnMonitorStateTransition(monitorType: GetShortName(monitorType), stateName: GetShortName(stateName), isEntry: isEntry, isInHotState: isInHotState);
         }
-
-        public override void OnCreateActor(ActorId id, string creatorName, string creatorType)
-        {
-            if (id.Name.Contains("GodMachine") || creatorName.Contains("GodMachine"))
-            {
-                return;
-            }
-
-            base.OnCreateActor(id, GetShortName(creatorName), creatorType);
-        }
-
+        
         public override void OnMonitorProcessEvent(string monitorType, string stateName, string senderName, string senderType,
             string senderStateName, Event e)
         {
@@ -90,7 +80,7 @@ public override void OnMonitorProcessEvent(string monitorType, string stateName,
             Logger.WriteLine(text);
         }
 
-        public override void OnDequeueEvent(ActorId id, string stateName, Event e)
+        public override void OnDequeueEvent(StateMachineId id, string stateName, Event e)
         {
             if (stateName.Contains("__InitState__") || id.Name.Contains("GodMachine"))
             {
@@ -112,7 +102,7 @@ public override void OnDequeueEvent(ActorId id, string stateName, Event e)
             Logger.WriteLine(text);
         }
 
-        public override void OnRaiseEvent(ActorId id, string stateName, Event e)
+        public override void OnRaiseEvent(StateMachineId id, string stateName, Event e)
         {
             stateName = GetShortName(stateName);
             var eventName = GetEventNameWithPayload(e);
@@ -134,9 +124,9 @@ public override void OnRaiseEvent(ActorId id, string stateName, Event e)
             Logger.WriteLine(text);
         }
 
-        public override void OnEnqueueEvent(ActorId id, Event e) {   }
+        public override void OnEnqueueEvent(StateMachineId id, Event e) {   }
 
-        public override void OnReceiveEvent(ActorId id, string stateName, Event e, bool wasBlocked)
+        public override void OnReceiveEvent(StateMachineId id, string stateName, Event e, bool wasBlocked)
         {
             stateName = GetShortName(stateName);
             var eventName = GetEventNameWithPayload(e);
@@ -162,18 +152,18 @@ public override void OnMonitorRaiseEvent(string monitorType, string stateName, E
             Logger.WriteLine(text);
         }
 
-        public override void OnSendEvent(ActorId targetActorId, string senderName, string senderType, string senderStateName, Event e, Guid opGroupId, bool isTargetHalted)
+        public override void OnSendEvent(StateMachineId targetStateMachineId, string senderName, string senderType, string senderStateName, Event e, Guid opGroupId, bool isTargetHalted)
         {
             senderStateName = GetShortName(senderStateName);
             var eventName = GetEventNameWithPayload(e);
             var opGroupIdMsg = opGroupId != Guid.Empty ? $" (operation group '{opGroupId}')" : string.Empty;
             var isHalted = isTargetHalted ? $" which has halted" : string.Empty;
             var sender = !string.IsNullOrEmpty(senderName) ? $"'{senderName}' in state '{senderStateName}'" : $"The runtime";
-            var text = $"<SendLog> {sender} sent event '{eventName}' to '{targetActorId}'{isHalted}{opGroupIdMsg}.";
+            var text = $"<SendLog> {sender} sent event '{eventName}' to '{targetStateMachineId}'{isHalted}{opGroupIdMsg}.";
             Logger.WriteLine(text);
         }
 
-        public override void OnGotoState(ActorId id, string currStateName, string newStateName)
+        public override void OnGotoState(StateMachineId id, string currStateName, string newStateName)
         {
             if (currStateName.Contains("__InitState__") || id.Name.Contains("GodMachine"))
             {
@@ -183,7 +173,7 @@ public override void OnGotoState(ActorId id, string currStateName, string newSta
             base.OnGotoState(id, GetShortName(currStateName), GetShortName(newStateName));
         }
 
-        public override void OnExecuteAction(ActorId id, string handlingStateName, string currentStateName, string actionName)
+        public override void OnExecuteAction(StateMachineId id, string handlingStateName, string currentStateName, string actionName)
         {
         }
 
@@ -191,7 +181,7 @@ public override void OnMonitorExecuteAction(string monitorType, string stateName
         {
         }
 
-        public override void OnExceptionHandled(ActorId id, string stateName, string actionName, Exception ex)
+        public override void OnExceptionHandled(StateMachineId id, string stateName, string actionName, Exception ex)
         {
             if (ex is PNonStandardReturnException)
             {
@@ -200,7 +190,7 @@ public override void OnExceptionHandled(ActorId id, string stateName, string act
             base.OnExceptionHandled(id: id, stateName: GetShortName(stateName), actionName: actionName, ex: ex);
         }
 
-        public override void OnExceptionThrown(ActorId id, string stateName, string actionName, Exception ex)
+        public override void OnExceptionThrown(StateMachineId id, string stateName, string actionName, Exception ex)
         {
             if (ex is PNonStandardReturnException)
             {
@@ -214,7 +204,7 @@ public override void OnCreateMonitor(string monitorType)
             base.OnCreateMonitor(GetShortName(monitorType));
         }
 
-        public override void OnHandleRaisedEvent(ActorId id, string stateName, Event e)
+        public override void OnHandleRaisedEvent(StateMachineId id, string stateName, Event e)
         {
         }
 
diff --git a/Src/PChecker/CheckerCore/PRuntime/PMachine.cs b/Src/PChecker/CheckerCore/PRuntime/PMachine.cs
index 92014533a..f0cf47b3c 100644
--- a/Src/PChecker/CheckerCore/PRuntime/PMachine.cs
+++ b/Src/PChecker/CheckerCore/PRuntime/PMachine.cs
@@ -2,10 +2,10 @@
 using System.Collections.Generic;
 using System.Linq;
 using System.Threading.Tasks;
-using PChecker.Actors;
-using PChecker.Actors.Events;
-using PChecker.Actors.Exceptions;
-using PChecker.Actors.Logging;
+using PChecker.StateMachines;
+using PChecker.StateMachines.Events;
+using PChecker.StateMachines.Exceptions;
+using PChecker.StateMachines.Logging;
 using PChecker.PRuntime.Exceptions;
 using PChecker.PRuntime.Values;
 
@@ -70,7 +70,7 @@ public PMachineValue CreateInterface<T>(PMachine creator, IPrtValue payload = nu
             Assert(creates.Contains(createdInterface),
                 $"Machine {GetType().Name} cannot create interface {createdInterface}, not in its creates set");
             var createMachine = PModule.interfaceDefinitionMap[createdInterface];
-            var machineId = CreateActor(createMachine, createdInterface.Substring(2),
+            var machineId = CreateStateMachine(createMachine, createdInterface.Substring(2),
                 new InitializeParametersEvent(new InitializeParameters(createdInterface, payload)));
             return new PMachineValue(machineId, PInterfaces.GetPermissions(createdInterface));
         }
diff --git a/Src/PChecker/CheckerCore/PRuntime/PModule.cs b/Src/PChecker/CheckerCore/PRuntime/PModule.cs
index 16cc35cee..d86cbc528 100644
--- a/Src/PChecker/CheckerCore/PRuntime/PModule.cs
+++ b/Src/PChecker/CheckerCore/PRuntime/PModule.cs
@@ -1,6 +1,6 @@
 using System;
 using System.Collections.Generic;
-using PChecker.Actors;
+using PChecker.StateMachines;
 
 namespace PChecker.PRuntime
 {
@@ -13,6 +13,6 @@ public class PModule
         public static IDictionary<string, Dictionary<string, string>> linkMap =
             new Dictionary<string, Dictionary<string, string>>();
 
-        public static IActorRuntime runtime;
+        public static IStateMachineRuntime runtime;
     }
 }
\ No newline at end of file
diff --git a/Src/PChecker/CheckerCore/PRuntime/PMonitor.cs b/Src/PChecker/CheckerCore/PRuntime/PMonitor.cs
index 08289f4cc..439542238 100644
--- a/Src/PChecker/CheckerCore/PRuntime/PMonitor.cs
+++ b/Src/PChecker/CheckerCore/PRuntime/PMonitor.cs
@@ -1,7 +1,7 @@
 using System.Collections.Generic;
 using System.Linq;
-using PChecker.Actors.Events;
-using PChecker.Actors.Logging;
+using PChecker.StateMachines.Events;
+using PChecker.StateMachines.Logging;
 using PChecker.Specifications.Monitors;
 
 namespace PChecker.PRuntime
diff --git a/Src/PChecker/CheckerCore/PRuntime/Values/PMachineValue.cs b/Src/PChecker/CheckerCore/PRuntime/Values/PMachineValue.cs
index 16c758c4d..624ee4a32 100644
--- a/Src/PChecker/CheckerCore/PRuntime/Values/PMachineValue.cs
+++ b/Src/PChecker/CheckerCore/PRuntime/Values/PMachineValue.cs
@@ -1,19 +1,19 @@
 using System.Collections.Generic;
 using System.Linq;
-using PChecker.Actors;
+using PChecker.StateMachines;
 
 namespace PChecker.PRuntime.Values
 {
     public class I_Main : PMachineValue
     {
-        public I_Main(ActorId machine, List<string> permissions) : base(machine, permissions)
+        public I_Main(StateMachineId machine, List<string> permissions) : base(machine, permissions)
         {
         }
     }
 
     public class PMachineValue : IPrtValue
     {
-        public PMachineValue(ActorId machine, List<string> permissions)
+        public PMachineValue(StateMachineId machine, List<string> permissions)
         {
             Id = machine;
             Permissions = permissions.ToList();
@@ -25,7 +25,7 @@ public PMachineValue(PMachineValue mValue)
             Permissions = mValue.Permissions.ToList();
         }
 
-        public ActorId Id { get; }
+        public StateMachineId Id { get; }
         public List<string> Permissions { get; }
 
         public bool Equals(IPrtValue other)
diff --git a/Src/PChecker/CheckerCore/Runtime/CoyoteRuntime.cs b/Src/PChecker/CheckerCore/Runtime/CoyoteRuntime.cs
index 058d314c3..73d26fc39 100644
--- a/Src/PChecker/CheckerCore/Runtime/CoyoteRuntime.cs
+++ b/Src/PChecker/CheckerCore/Runtime/CoyoteRuntime.cs
@@ -7,7 +7,7 @@
 using System.IO;
 using System.Threading;
 using System.Threading.Tasks;
-using PChecker.Actors.Events;
+using PChecker.StateMachines.Events;
 using PChecker.Exceptions;
 using PChecker.Random;
 using Monitor = PChecker.Specifications.Monitors.Monitor;
@@ -35,7 +35,7 @@ internal abstract class CoyoteRuntime : ICoyoteRuntime
                                                  (IsExecutionControlled ? throw new InvalidOperationException(string.Format(CultureInfo.InvariantCulture,
                                                          "Uncontrolled task '{0}' invoked a runtime method. Please make sure to avoid using concurrency APIs " +
                                                          "(e.g. 'Task.Run', 'Task.Delay' or 'Task.Yield' from the 'System.Threading.Tasks' namespace) inside " +
-                                                         "actor handlers or controlled tasks. If you are using external libraries that are executing concurrently, " +
+                                                         "state machine handlers or controlled tasks. If you are using external libraries that are executing concurrently, " +
                                                          "you will need to mock them during testing.",
                                                          Task.CurrentId.HasValue ? Task.CurrentId.Value.ToString() : "<unknown>")) :
                                                      RuntimeFactory.InstalledRuntime);
@@ -273,7 +273,7 @@ internal virtual void WrapAndThrowException(Exception exception, string s, param
         }
 
         /// <summary>
-        /// Terminates the runtime and notifies each active actor to halt execution.
+        /// Terminates the runtime and notifies each active state machine to halt execution.
         /// </summary>
         public void Stop() => IsRunning = false;
 
diff --git a/Src/PChecker/CheckerCore/Runtime/ICoyoteRuntime.cs b/Src/PChecker/CheckerCore/Runtime/ICoyoteRuntime.cs
index 72795194c..e5b72ff20 100644
--- a/Src/PChecker/CheckerCore/Runtime/ICoyoteRuntime.cs
+++ b/Src/PChecker/CheckerCore/Runtime/ICoyoteRuntime.cs
@@ -3,7 +3,7 @@
 
 using System;
 using System.IO;
-using PChecker.Actors.Events;
+using PChecker.StateMachines.Events;
 using PChecker.Exceptions;
 using PChecker.Specifications.Monitors;
 
@@ -129,7 +129,7 @@ void Monitor<T>(Event e)
         TextWriter SetLogger(TextWriter logger);
 
         /// <summary>
-        /// Terminates the runtime and notifies each active actor to halt execution.
+        /// Terminates the runtime and notifies each active state machine to halt execution.
         /// </summary>
         void Stop();
     }
diff --git a/Src/PChecker/CheckerCore/Runtime/RuntimeFactory.cs b/Src/PChecker/CheckerCore/Runtime/RuntimeFactory.cs
index 07c60cda0..f7c03b7b4 100644
--- a/Src/PChecker/CheckerCore/Runtime/RuntimeFactory.cs
+++ b/Src/PChecker/CheckerCore/Runtime/RuntimeFactory.cs
@@ -1,7 +1,7 @@
 // Copyright (c) Microsoft Corporation.
 // Licensed under the MIT License.
 
-using PChecker.Actors;
+using PChecker.StateMachines;
 using PChecker.Random;
 using PChecker.SystematicTesting;
 using PChecker.SystematicTesting.Strategies.Probabilistic;
diff --git a/Src/PChecker/CheckerCore/Specifications/CachedDelegate.cs b/Src/PChecker/CheckerCore/Specifications/CachedDelegate.cs
index e6fae4cda..70c4489c3 100644
--- a/Src/PChecker/CheckerCore/Specifications/CachedDelegate.cs
+++ b/Src/PChecker/CheckerCore/Specifications/CachedDelegate.cs
@@ -3,7 +3,7 @@
 
 using System;
 using System.Reflection;
-using PChecker.Actors.Events;
+using PChecker.StateMachines.Events;
 
 namespace PChecker.Specifications.Monitors
 {
diff --git a/Src/PChecker/CheckerCore/Specifications/Monitor.cs b/Src/PChecker/CheckerCore/Specifications/Monitor.cs
index 5674815c7..b8e2020d4 100644
--- a/Src/PChecker/CheckerCore/Specifications/Monitor.cs
+++ b/Src/PChecker/CheckerCore/Specifications/Monitor.cs
@@ -10,11 +10,11 @@
 using System.Linq.Expressions;
 using System.Reflection;
 using System.Threading.Tasks;
-using PChecker.Actors;
-using PChecker.Actors.Events;
-using PChecker.Actors.Handlers;
-using PChecker.Actors.Logging;
-using PChecker.Actors.StateTransitions;
+using PChecker.StateMachines;
+using PChecker.StateMachines.Events;
+using PChecker.StateMachines.Handlers;
+using PChecker.StateMachines.Logging;
+using PChecker.StateMachines.StateTransitions;
 using PChecker.Exceptions;
 using PChecker.SystematicTesting;
 
@@ -49,7 +49,7 @@ public abstract class Monitor
 
         /// <summary>
         /// A set of lockable objects used to protect static initialization of the ActionCache while
-        /// also enabling multithreaded initialization of different Actor types.
+        /// also enabling multithreaded initialization of different StateMachine types.
         /// </summary>
         private static readonly ConcurrentDictionary<Type, object> ActionCacheLocks =
             new ConcurrentDictionary<Type, object>();
@@ -703,7 +703,7 @@ internal void InitializeStateInformation()
             var syncObject = ActionCacheLocks.GetOrAdd(monitorType, _ => new object());
 
             // Locking this syncObject ensures only one thread enters the initialization code to update
-            // the ActionCache for this specific Actor type.
+            // the ActionCache for this specific StateMachine type.
             lock (syncObject)
             {
                 if (MonitorActionMap.ContainsKey(monitorType))
diff --git a/Src/PChecker/CheckerCore/Actors/EventQueues/DequeueStatus.cs b/Src/PChecker/CheckerCore/StateMachines/EventQueues/DequeueStatus.cs
similarity index 93%
rename from Src/PChecker/CheckerCore/Actors/EventQueues/DequeueStatus.cs
rename to Src/PChecker/CheckerCore/StateMachines/EventQueues/DequeueStatus.cs
index 6482634a4..8ef2d174d 100644
--- a/Src/PChecker/CheckerCore/Actors/EventQueues/DequeueStatus.cs
+++ b/Src/PChecker/CheckerCore/StateMachines/EventQueues/DequeueStatus.cs
@@ -1,7 +1,7 @@
 // Copyright (c) Microsoft Corporation.
 // Licensed under the MIT License.
 
-namespace PChecker.Actors.EventQueues
+namespace PChecker.StateMachines.EventQueues
 {
     /// <summary>
     /// The status returned as the result of a dequeue operation.
diff --git a/Src/PChecker/CheckerCore/Actors/EventQueues/EnqueueStatus.cs b/Src/PChecker/CheckerCore/StateMachines/EventQueues/EnqueueStatus.cs
similarity index 94%
rename from Src/PChecker/CheckerCore/Actors/EventQueues/EnqueueStatus.cs
rename to Src/PChecker/CheckerCore/StateMachines/EventQueues/EnqueueStatus.cs
index 57aab56ab..5fd5941d3 100644
--- a/Src/PChecker/CheckerCore/Actors/EventQueues/EnqueueStatus.cs
+++ b/Src/PChecker/CheckerCore/StateMachines/EventQueues/EnqueueStatus.cs
@@ -1,7 +1,7 @@
 // Copyright (c) Microsoft Corporation.
 // Licensed under the MIT License.
 
-namespace PChecker.Actors.EventQueues
+namespace PChecker.StateMachines.EventQueues
 {
     /// <summary>
     /// The status returned as the result of an enqueue operation.
diff --git a/Src/PChecker/CheckerCore/Actors/EventQueues/EventQueue.cs b/Src/PChecker/CheckerCore/StateMachines/EventQueues/EventQueue.cs
similarity index 93%
rename from Src/PChecker/CheckerCore/Actors/EventQueues/EventQueue.cs
rename to Src/PChecker/CheckerCore/StateMachines/EventQueues/EventQueue.cs
index a02fe0085..bfa6d5dfe 100644
--- a/Src/PChecker/CheckerCore/Actors/EventQueues/EventQueue.cs
+++ b/Src/PChecker/CheckerCore/StateMachines/EventQueues/EventQueue.cs
@@ -5,10 +5,10 @@
 using System.Collections.Generic;
 using System.Linq;
 using System.Threading.Tasks;
-using PChecker.Actors.Events;
-using PChecker.Actors.Managers;
+using PChecker.StateMachines.Events;
+using PChecker.StateMachines.Managers;
 
-namespace PChecker.Actors.EventQueues.Mocks
+namespace PChecker.StateMachines.EventQueues.Mocks
 {
     /// <summary>
     /// Implements a queue of events that is used during testing.
@@ -16,14 +16,14 @@ namespace PChecker.Actors.EventQueues.Mocks
     internal sealed class EventQueue : IEventQueue
     {
         /// <summary>
-        /// Manages the actor that owns this queue.
+        /// Manages the state machine that owns this queue.
         /// </summary>
         private readonly IStateMachineManager StateMachineManager;
 
         /// <summary>
-        /// The actor that owns this queue.
+        /// The state machine that owns this queue.
         /// </summary>
-        private readonly StateMachine Actor;
+        private readonly StateMachine StateMachine;
 
         /// <summary>
         /// The internal queue that contains events with their metadata.
@@ -66,10 +66,10 @@ internal sealed class EventQueue : IEventQueue
         /// <summary>
         /// Initializes a new instance of the <see cref="EventQueue"/> class.
         /// </summary>
-        internal EventQueue(IStateMachineManager stateMachineManager, StateMachine actor)
+        internal EventQueue(IStateMachineManager stateMachineManager, StateMachine stateMachine)
         {
             StateMachineManager = stateMachineManager;
-            Actor = actor;
+            StateMachine = stateMachine;
             Queue = new LinkedList<(Event, Guid, EventInfo)>();
             EventWaitTypes = new Dictionary<Type, Func<Event, bool>>();
             IsClosed = false;
@@ -135,7 +135,7 @@ public EnqueueStatus Enqueue(Event e, Guid opGroupId, EventInfo info)
             var hasDefaultHandler = StateMachineManager.IsDefaultHandlerAvailable();
             if (hasDefaultHandler)
             {
-                Actor.Runtime.NotifyDefaultEventHandlerCheck(Actor);
+                StateMachine.Runtime.NotifyDefaultEventHandlerCheck(StateMachine);
             }
 
             // Try to dequeue the next event, if there is one.
@@ -156,8 +156,8 @@ public EnqueueStatus Enqueue(Event e, Guid opGroupId, EventInfo info)
 
             // TODO: check op-id of default event.
             // A default event handler exists.
-            var stateName = NameResolver.GetStateNameForLogging(Actor.CurrentState.GetType());
-            var eventOrigin = new EventOriginInfo(Actor.Id, Actor.GetType().FullName, stateName);
+            var stateName = NameResolver.GetStateNameForLogging(StateMachine.CurrentState.GetType());
+            var eventOrigin = new EventOriginInfo(StateMachine.Id, StateMachine.GetType().FullName, stateName);
             return (DequeueStatus.Default, DefaultEvent.Instance, Guid.Empty, new EventInfo(DefaultEvent.Instance, eventOrigin));
         }
 
@@ -208,8 +208,8 @@ public EnqueueStatus Enqueue(Event e, Guid opGroupId, EventInfo info)
         /// <inheritdoc/>
         public void RaiseEvent(Event e, Guid opGroupId)
         {
-            var stateName = NameResolver.GetStateNameForLogging(Actor.CurrentState.GetType());
-            var eventOrigin = new EventOriginInfo(Actor.Id, Actor.GetType().FullName, stateName);
+            var stateName = NameResolver.GetStateNameForLogging(StateMachine.CurrentState.GetType());
+            var eventOrigin = new EventOriginInfo(StateMachine.Id, StateMachine.GetType().FullName, stateName);
             var info = new EventInfo(e, eventOrigin);
             RaisedEvent = (e, opGroupId, info);
             StateMachineManager.OnRaiseEvent(e, opGroupId, info);
@@ -255,7 +255,7 @@ public Task<Event> ReceiveEventAsync(params Tuple<Type, Func<Event, bool>>[] eve
         /// </summary>
         private Task<Event> ReceiveEventAsync(Dictionary<Type, Func<Event, bool>> eventWaitTypes)
         {
-            Actor.Runtime.NotifyReceiveCalled(Actor);
+            StateMachine.Runtime.NotifyReceiveCalled(StateMachine);
 
             (Event e, Guid opGroupId, EventInfo info) receivedEvent = default;
             var node = Queue.First;
diff --git a/Src/PChecker/CheckerCore/Actors/EventQueues/IEventQueue.cs b/Src/PChecker/CheckerCore/StateMachines/EventQueues/IEventQueue.cs
similarity index 95%
rename from Src/PChecker/CheckerCore/Actors/EventQueues/IEventQueue.cs
rename to Src/PChecker/CheckerCore/StateMachines/EventQueues/IEventQueue.cs
index 20026e59c..c449792ae 100644
--- a/Src/PChecker/CheckerCore/Actors/EventQueues/IEventQueue.cs
+++ b/Src/PChecker/CheckerCore/StateMachines/EventQueues/IEventQueue.cs
@@ -3,9 +3,9 @@
 
 using System;
 using System.Threading.Tasks;
-using PChecker.Actors.Events;
+using PChecker.StateMachines.Events;
 
-namespace PChecker.Actors.EventQueues
+namespace PChecker.StateMachines.EventQueues
 {
     /// <summary>
     /// Interface of a queue of events.
diff --git a/Src/PChecker/CheckerCore/Actors/Events/DefaultEvent.cs b/Src/PChecker/CheckerCore/StateMachines/Events/DefaultEvent.cs
similarity index 94%
rename from Src/PChecker/CheckerCore/Actors/Events/DefaultEvent.cs
rename to Src/PChecker/CheckerCore/StateMachines/Events/DefaultEvent.cs
index bf430e673..3ad12575d 100644
--- a/Src/PChecker/CheckerCore/Actors/Events/DefaultEvent.cs
+++ b/Src/PChecker/CheckerCore/StateMachines/Events/DefaultEvent.cs
@@ -3,7 +3,7 @@
 
 using System.Runtime.Serialization;
 
-namespace PChecker.Actors.Events
+namespace PChecker.StateMachines.Events
 {
     /// <summary>
     /// A default event that is generated by the runtime when
diff --git a/Src/PChecker/CheckerCore/Actors/Events/Event.cs b/Src/PChecker/CheckerCore/StateMachines/Events/Event.cs
similarity index 86%
rename from Src/PChecker/CheckerCore/Actors/Events/Event.cs
rename to Src/PChecker/CheckerCore/StateMachines/Events/Event.cs
index a33f29817..1567ec597 100644
--- a/Src/PChecker/CheckerCore/Actors/Events/Event.cs
+++ b/Src/PChecker/CheckerCore/StateMachines/Events/Event.cs
@@ -3,7 +3,7 @@
 
 using System.Runtime.Serialization;
 
-namespace PChecker.Actors.Events
+namespace PChecker.StateMachines.Events
 {
     /// <summary>
     /// Abstract class representing an event.
diff --git a/Src/PChecker/CheckerCore/Actors/Events/EventInfo.cs b/Src/PChecker/CheckerCore/StateMachines/Events/EventInfo.cs
similarity index 96%
rename from Src/PChecker/CheckerCore/Actors/Events/EventInfo.cs
rename to Src/PChecker/CheckerCore/StateMachines/Events/EventInfo.cs
index b12f117d6..ff6695c2c 100644
--- a/Src/PChecker/CheckerCore/Actors/Events/EventInfo.cs
+++ b/Src/PChecker/CheckerCore/StateMachines/Events/EventInfo.cs
@@ -3,7 +3,7 @@
 
 using System.Runtime.Serialization;
 
-namespace PChecker.Actors.Events
+namespace PChecker.StateMachines.Events
 {
     /// <summary>
     /// Contains an <see cref="Event"/>, and its associated metadata.
diff --git a/Src/PChecker/CheckerCore/Actors/Events/EventOriginInfo.cs b/Src/PChecker/CheckerCore/StateMachines/Events/EventOriginInfo.cs
similarity index 61%
rename from Src/PChecker/CheckerCore/Actors/Events/EventOriginInfo.cs
rename to Src/PChecker/CheckerCore/StateMachines/Events/EventOriginInfo.cs
index 8aea77ed5..8d56cc8a1 100644
--- a/Src/PChecker/CheckerCore/Actors/Events/EventOriginInfo.cs
+++ b/Src/PChecker/CheckerCore/StateMachines/Events/EventOriginInfo.cs
@@ -3,7 +3,7 @@
 
 using System.Runtime.Serialization;
 
-namespace PChecker.Actors.Events
+namespace PChecker.StateMachines.Events
 {
     /// <summary>
     /// Contains the origin information of an <see cref="Event"/>.
@@ -12,16 +12,16 @@ namespace PChecker.Actors.Events
     internal class EventOriginInfo
     {
         /// <summary>
-        /// The sender actor id.
+        /// The sender state machine id.
         /// </summary>
         [DataMember]
-        internal ActorId SenderActorId { get; private set; }
+        internal StateMachineId SenderStateMachineId { get; private set; }
 
         /// <summary>
-        /// The sender actor name.
+        /// The sender state machine name.
         /// </summary>
         [DataMember]
-        internal string SenderActorName { get; private set; }
+        internal string SenderStateMachineName { get; private set; }
 
         /// <summary>
         /// The sender state name, if there is one.
@@ -32,10 +32,10 @@ internal class EventOriginInfo
         /// <summary>
         /// Initializes a new instance of the <see cref="EventOriginInfo"/> class.
         /// </summary>
-        internal EventOriginInfo(ActorId senderActorId, string senderMachineName, string senderStateName)
+        internal EventOriginInfo(StateMachineId senderStateMachineId, string senderMachineName, string senderStateName)
         {
-            SenderActorId = senderActorId;
-            SenderActorName = senderMachineName;
+            SenderStateMachineId = senderStateMachineId;
+            SenderStateMachineName = senderMachineName;
             SenderStateName = senderStateName;
         }
     }
diff --git a/Src/PChecker/CheckerCore/Actors/Events/GotoStateEvent.cs b/Src/PChecker/CheckerCore/StateMachines/Events/GotoStateEvent.cs
similarity index 94%
rename from Src/PChecker/CheckerCore/Actors/Events/GotoStateEvent.cs
rename to Src/PChecker/CheckerCore/StateMachines/Events/GotoStateEvent.cs
index ef8eadf02..d77da5dff 100644
--- a/Src/PChecker/CheckerCore/Actors/Events/GotoStateEvent.cs
+++ b/Src/PChecker/CheckerCore/StateMachines/Events/GotoStateEvent.cs
@@ -4,7 +4,7 @@
 using System;
 using System.Runtime.Serialization;
 
-namespace PChecker.Actors.Events
+namespace PChecker.StateMachines.Events
 {
     /// <summary>
     /// The goto state event.
diff --git a/Src/PChecker/CheckerCore/Actors/Events/HaltEvent.cs b/Src/PChecker/CheckerCore/StateMachines/Events/HaltEvent.cs
similarity index 93%
rename from Src/PChecker/CheckerCore/Actors/Events/HaltEvent.cs
rename to Src/PChecker/CheckerCore/StateMachines/Events/HaltEvent.cs
index e1dcc6e06..659d3ca1b 100644
--- a/Src/PChecker/CheckerCore/Actors/Events/HaltEvent.cs
+++ b/Src/PChecker/CheckerCore/StateMachines/Events/HaltEvent.cs
@@ -3,7 +3,7 @@
 
 using System.Runtime.Serialization;
 
-namespace PChecker.Actors.Events
+namespace PChecker.StateMachines.Events
 {
     /// <summary>
     /// The halt event.
diff --git a/Src/PChecker/CheckerCore/Actors/Events/QuiescentEvent.cs b/Src/PChecker/CheckerCore/StateMachines/Events/QuiescentEvent.cs
similarity index 52%
rename from Src/PChecker/CheckerCore/Actors/Events/QuiescentEvent.cs
rename to Src/PChecker/CheckerCore/StateMachines/Events/QuiescentEvent.cs
index 9b0649273..1746853d1 100644
--- a/Src/PChecker/CheckerCore/Actors/Events/QuiescentEvent.cs
+++ b/Src/PChecker/CheckerCore/StateMachines/Events/QuiescentEvent.cs
@@ -3,26 +3,26 @@
 
 using System.Runtime.Serialization;
 
-namespace PChecker.Actors.Events
+namespace PChecker.StateMachines.Events
 {
     /// <summary>
-    /// Signals that an actor has reached quiescence.
+    /// Signals that an state machine has reached quiescence.
     /// </summary>
     [DataContract]
     internal sealed class QuiescentEvent : Event
     {
         /// <summary>
-        /// The id of the actor that has reached quiescence.
+        /// The id of the state machine that has reached quiescence.
         /// </summary>
-        public ActorId ActorId;
+        public StateMachineId StateMachineId;
 
         /// <summary>
         /// Initializes a new instance of the <see cref="QuiescentEvent"/> class.
         /// </summary>
-        /// <param name="id">The id of the actor that has reached quiescence.</param>
-        public QuiescentEvent(ActorId id)
+        /// <param name="id">The id of the state machine that has reached quiescence.</param>
+        public QuiescentEvent(StateMachineId id)
         {
-            ActorId = id;
+            StateMachineId = id;
         }
     }
 }
\ No newline at end of file
diff --git a/Src/PChecker/CheckerCore/Actors/Events/WildcardEvent.cs b/Src/PChecker/CheckerCore/StateMachines/Events/WildcardEvent.cs
similarity index 92%
rename from Src/PChecker/CheckerCore/Actors/Events/WildcardEvent.cs
rename to Src/PChecker/CheckerCore/StateMachines/Events/WildcardEvent.cs
index bba77fd07..6c2c0dff9 100644
--- a/Src/PChecker/CheckerCore/Actors/Events/WildcardEvent.cs
+++ b/Src/PChecker/CheckerCore/StateMachines/Events/WildcardEvent.cs
@@ -3,7 +3,7 @@
 
 using System.Runtime.Serialization;
 
-namespace PChecker.Actors.Events
+namespace PChecker.StateMachines.Events
 {
     /// <summary>
     /// The wild card event.
diff --git a/Src/PChecker/CheckerCore/Actors/Exceptions/ActionExceptionFilterException.cs b/Src/PChecker/CheckerCore/StateMachines/Exceptions/ActionExceptionFilterException.cs
similarity index 96%
rename from Src/PChecker/CheckerCore/Actors/Exceptions/ActionExceptionFilterException.cs
rename to Src/PChecker/CheckerCore/StateMachines/Exceptions/ActionExceptionFilterException.cs
index afb53fae9..fecdc6114 100644
--- a/Src/PChecker/CheckerCore/Actors/Exceptions/ActionExceptionFilterException.cs
+++ b/Src/PChecker/CheckerCore/StateMachines/Exceptions/ActionExceptionFilterException.cs
@@ -4,7 +4,7 @@
 using System;
 using PChecker.Exceptions;
 
-namespace PChecker.Actors.Exceptions
+namespace PChecker.StateMachines.Exceptions
 {
     /// <summary>
     /// Exception that is thrown by the runtime upon an <see cref="StateMachine"/> action failure.
diff --git a/Src/PChecker/CheckerCore/StateMachines/Exceptions/OnEventDroppedHandler.cs b/Src/PChecker/CheckerCore/StateMachines/Exceptions/OnEventDroppedHandler.cs
new file mode 100644
index 000000000..df4b14eae
--- /dev/null
+++ b/Src/PChecker/CheckerCore/StateMachines/Exceptions/OnEventDroppedHandler.cs
@@ -0,0 +1,12 @@
+// Copyright (c) Microsoft Corporation.
+// Licensed under the MIT License.
+
+using PChecker.StateMachines.Events;
+
+namespace PChecker.StateMachines.Exceptions
+{
+    /// <summary>
+    /// Handles the <see cref="IStateMachineRuntime.OnEventDropped"/> event.
+    /// </summary>
+    public delegate void OnEventDroppedHandler(Event e, StateMachineId target);
+}
\ No newline at end of file
diff --git a/Src/PChecker/CheckerCore/Actors/Exceptions/OnExceptionOutcome.cs b/Src/PChecker/CheckerCore/StateMachines/Exceptions/OnExceptionOutcome.cs
similarity index 63%
rename from Src/PChecker/CheckerCore/Actors/Exceptions/OnExceptionOutcome.cs
rename to Src/PChecker/CheckerCore/StateMachines/Exceptions/OnExceptionOutcome.cs
index 1a09282f5..1073244c4 100644
--- a/Src/PChecker/CheckerCore/Actors/Exceptions/OnExceptionOutcome.cs
+++ b/Src/PChecker/CheckerCore/StateMachines/Exceptions/OnExceptionOutcome.cs
@@ -1,7 +1,7 @@
 // Copyright (c) Microsoft Corporation.
 // Licensed under the MIT License.
 
-namespace PChecker.Actors.Exceptions
+namespace PChecker.StateMachines.Exceptions
 {
     /// <summary>
     /// The outcome when an <see cref="StateMachine"/> throws an exception.
@@ -9,17 +9,17 @@ namespace PChecker.Actors.Exceptions
     public enum OnExceptionOutcome
     {
         /// <summary>
-        /// The actor throws the exception causing the runtime to fail.
+        /// The state machine throws the exception causing the runtime to fail.
         /// </summary>
         ThrowException = 0,
 
         /// <summary>
-        /// The actor handles the exception and resumes execution.
+        /// The state machine handles the exception and resumes execution.
         /// </summary>
         HandledException = 1,
 
         /// <summary>
-        /// The actor handles the exception and halts.
+        /// The state machine handles the exception and halts.
         /// </summary>
         Halt = 2
     }
diff --git a/Src/PChecker/CheckerCore/Actors/Exceptions/UnhandledEventException.cs b/Src/PChecker/CheckerCore/StateMachines/Exceptions/UnhandledEventException.cs
similarity index 84%
rename from Src/PChecker/CheckerCore/Actors/Exceptions/UnhandledEventException.cs
rename to Src/PChecker/CheckerCore/StateMachines/Exceptions/UnhandledEventException.cs
index d9a23b780..38bec73ea 100644
--- a/Src/PChecker/CheckerCore/Actors/Exceptions/UnhandledEventException.cs
+++ b/Src/PChecker/CheckerCore/StateMachines/Exceptions/UnhandledEventException.cs
@@ -1,10 +1,10 @@
 // Copyright (c) Microsoft Corporation.
 // Licensed under the MIT License.
 
-using PChecker.Actors.Events;
+using PChecker.StateMachines.Events;
 using PChecker.Exceptions;
 
-namespace PChecker.Actors.Exceptions
+namespace PChecker.StateMachines.Exceptions
 {
     /// <summary>
     /// Signals that an <see cref="StateMachine"/> received an unhandled event.
@@ -17,7 +17,7 @@ public sealed class UnhandledEventException : RuntimeException
         public Event UnhandledEvent;
 
         /// <summary>
-        /// The name of the current state, if the actor that threw the exception
+        /// The name of the current state, if the state machine that threw the exception
         /// is a <see cref="StateMachine"/> and a state exists, else null.
         /// </summary>
         public string CurrentStateName;
@@ -26,7 +26,7 @@ public sealed class UnhandledEventException : RuntimeException
         /// Initializes a new instance of the <see cref="UnhandledEventException"/> class.
         /// </summary>
         /// <param name="unhandledEvent">The event that was unhandled.</param>
-        /// <param name="currentStateName">The name of the current state, if the actor that threw the exception
+        /// <param name="currentStateName">The name of the current state, if the state machine that threw the exception
         /// is a state machine and a state exists, else null.</param>
         /// <param name="message">The exception message.</param>
         internal UnhandledEventException(Event unhandledEvent, string currentStateName, string message)
diff --git a/Src/PChecker/CheckerCore/Actors/Handlers/ActionEventHandlerDeclaration.cs b/Src/PChecker/CheckerCore/StateMachines/Handlers/ActionEventHandlerDeclaration.cs
similarity index 94%
rename from Src/PChecker/CheckerCore/Actors/Handlers/ActionEventHandlerDeclaration.cs
rename to Src/PChecker/CheckerCore/StateMachines/Handlers/ActionEventHandlerDeclaration.cs
index eb8a3aa1d..6cb1e69de 100644
--- a/Src/PChecker/CheckerCore/Actors/Handlers/ActionEventHandlerDeclaration.cs
+++ b/Src/PChecker/CheckerCore/StateMachines/Handlers/ActionEventHandlerDeclaration.cs
@@ -1,7 +1,7 @@
 // Copyright (c) Microsoft Corporation.
 // Licensed under the MIT License.
 
-namespace PChecker.Actors.Handlers
+namespace PChecker.StateMachines.Handlers
 {
     /// <summary>
     /// Defines an action event handler declaration.
diff --git a/Src/PChecker/CheckerCore/Actors/Handlers/CachedDelegate.cs b/Src/PChecker/CheckerCore/StateMachines/Handlers/CachedDelegate.cs
similarity index 90%
rename from Src/PChecker/CheckerCore/Actors/Handlers/CachedDelegate.cs
rename to Src/PChecker/CheckerCore/StateMachines/Handlers/CachedDelegate.cs
index 1d69e9511..895b68ba5 100644
--- a/Src/PChecker/CheckerCore/Actors/Handlers/CachedDelegate.cs
+++ b/Src/PChecker/CheckerCore/StateMachines/Handlers/CachedDelegate.cs
@@ -4,12 +4,12 @@
 using System;
 using System.Reflection;
 using System.Threading.Tasks;
-using PChecker.Actors.Events;
+using PChecker.StateMachines.Events;
 
-namespace PChecker.Actors.Handlers
+namespace PChecker.StateMachines.Handlers
 {
     /// <summary>
-    /// An actor delegate that has been cached to optimize performance of invocations.
+    /// An state machine delegate that has been cached to optimize performance of invocations.
     /// </summary>
     internal class CachedDelegate
     {
diff --git a/Src/PChecker/CheckerCore/Actors/Handlers/DeferEventHandlerDeclaration.cs b/Src/PChecker/CheckerCore/StateMachines/Handlers/DeferEventHandlerDeclaration.cs
similarity index 88%
rename from Src/PChecker/CheckerCore/Actors/Handlers/DeferEventHandlerDeclaration.cs
rename to Src/PChecker/CheckerCore/StateMachines/Handlers/DeferEventHandlerDeclaration.cs
index 428426ed4..76ed42123 100644
--- a/Src/PChecker/CheckerCore/Actors/Handlers/DeferEventHandlerDeclaration.cs
+++ b/Src/PChecker/CheckerCore/StateMachines/Handlers/DeferEventHandlerDeclaration.cs
@@ -1,7 +1,7 @@
 // Copyright (c) Microsoft Corporation.
 // Licensed under the MIT License.
 
-namespace PChecker.Actors.Handlers
+namespace PChecker.StateMachines.Handlers
 {
     /// <summary>
     /// Defines a defer event handler declaration.
diff --git a/Src/PChecker/CheckerCore/Actors/Handlers/EventHandlerDeclaration.cs b/Src/PChecker/CheckerCore/StateMachines/Handlers/EventHandlerDeclaration.cs
similarity index 87%
rename from Src/PChecker/CheckerCore/Actors/Handlers/EventHandlerDeclaration.cs
rename to Src/PChecker/CheckerCore/StateMachines/Handlers/EventHandlerDeclaration.cs
index 870fae0ca..4bfb5b23d 100644
--- a/Src/PChecker/CheckerCore/Actors/Handlers/EventHandlerDeclaration.cs
+++ b/Src/PChecker/CheckerCore/StateMachines/Handlers/EventHandlerDeclaration.cs
@@ -1,7 +1,7 @@
 // Copyright (c) Microsoft Corporation.
 // Licensed under the MIT License.
 
-namespace PChecker.Actors.Handlers
+namespace PChecker.StateMachines.Handlers
 {
     /// <summary>
     /// An abstract event handler declaration.
diff --git a/Src/PChecker/CheckerCore/Actors/Handlers/IgnoreEventHandlerDeclaration.cs b/Src/PChecker/CheckerCore/StateMachines/Handlers/IgnoreEventHandlerDeclaration.cs
similarity index 88%
rename from Src/PChecker/CheckerCore/Actors/Handlers/IgnoreEventHandlerDeclaration.cs
rename to Src/PChecker/CheckerCore/StateMachines/Handlers/IgnoreEventHandlerDeclaration.cs
index 0486c36c0..e7146ba15 100644
--- a/Src/PChecker/CheckerCore/Actors/Handlers/IgnoreEventHandlerDeclaration.cs
+++ b/Src/PChecker/CheckerCore/StateMachines/Handlers/IgnoreEventHandlerDeclaration.cs
@@ -1,7 +1,7 @@
 // Copyright (c) Microsoft Corporation.
 // Licensed under the MIT License.
 
-namespace PChecker.Actors.Handlers
+namespace PChecker.StateMachines.Handlers
 {
     /// <summary>
     /// Defines an ignore event handler declaration.
diff --git a/Src/PChecker/CheckerCore/StateMachines/IStateMachineRuntime.cs b/Src/PChecker/CheckerCore/StateMachines/IStateMachineRuntime.cs
new file mode 100644
index 000000000..c1b3ae751
--- /dev/null
+++ b/Src/PChecker/CheckerCore/StateMachines/IStateMachineRuntime.cs
@@ -0,0 +1,158 @@
+// Copyright (c) Microsoft Corporation.
+// Licensed under the MIT License.
+
+using System;
+using System.Threading.Tasks;
+using PChecker.StateMachines.Events;
+using PChecker.StateMachines.Exceptions;
+using PChecker.StateMachines.Logging;
+using PChecker.Runtime;
+
+namespace PChecker.StateMachines
+{
+    /// <summary>
+    /// Interface that exposes runtime methods for creating and executing state machines.
+    /// </summary>
+    public interface IStateMachineRuntime : ICoyoteRuntime
+    {
+        /// <summary>
+        /// Callback that is fired when an event is dropped.
+        /// </summary>
+        event OnEventDroppedHandler OnEventDropped;
+
+        /// <summary>
+        /// Creates a fresh state machine id that has not yet been bound to any state machine.
+        /// </summary>
+        /// <param name="type">Type of the state machine.</param>
+        /// <param name="name">Optional name used for logging.</param>
+        /// <returns>The result is the state machine id.</returns>
+        StateMachineId CreateStateMachineId(Type type, string name = null);
+
+        /// <summary>
+        /// Creates a state machine id that is uniquely tied to the specified unique name. The
+        /// returned state machine id can either be a fresh id (not yet bound to any state machine), or
+        /// it can be bound to a previously created state machine. In the second case, this state machine
+        /// id can be directly used to communicate with the corresponding state machine.
+        /// </summary>
+        /// <param name="type">Type of the state machine.</param>
+        /// <param name="name">Unique name used to create or get the state machine id.</param>
+        /// <returns>The result is the state machine id.</returns>
+        StateMachineId CreateStateMachineIdFromName(Type type, string name);
+
+        /// <summary>
+        /// Creates a new state machine of the specified <see cref="Type"/> and with the specified
+        /// optional <see cref="Event"/>. This event can only be used to access its payload,
+        /// and cannot be handled.
+        /// </summary>
+        /// <param name="type">Type of the state machine.</param>
+        /// <param name="initialEvent">Optional event used during initialization.</param>
+        /// <param name="opGroupId">Optional id that can be used to identify this operation.</param>
+        /// <returns>The result is the state machine id.</returns>
+        StateMachineId CreateStateMachine(Type type, Event initialEvent = null, Guid opGroupId = default);
+
+        /// <summary>
+        /// Creates a new state machine of the specified <see cref="Type"/> and name, and with the
+        /// specified optional <see cref="Event"/>. This event can only be used to access
+        /// its payload, and cannot be handled.
+        /// </summary>
+        /// <param name="type">Type of the state machine.</param>
+        /// <param name="name">Optional name used for logging.</param>
+        /// <param name="initialEvent">Optional event used during initialization.</param>
+        /// <param name="opGroupId">Optional id that can be used to identify this operation.</param>
+        /// <returns>The result is the state machine id.</returns>
+        StateMachineId CreateStateMachine(Type type, string name, Event initialEvent = null, Guid opGroupId = default);
+
+        /// <summary>
+        /// Creates a new state machine of the specified type, using the specified <see cref="StateMachineId"/>.
+        /// This method optionally passes an <see cref="Event"/> to the new state machine, which can only
+        /// be used to access its payload, and cannot be handled.
+        /// </summary>
+        /// <param name="id">Unbound state machine id.</param>
+        /// <param name="type">Type of the state machine.</param>
+        /// <param name="initialEvent">Optional event used during initialization.</param>
+        /// <param name="opGroupId">Optional id that can be used to identify this operation.</param>
+        /// <returns>The result is the state machine id.</returns>
+        StateMachineId CreateStateMachine(StateMachineId id, Type type, Event initialEvent = null, Guid opGroupId = default);
+
+        /// <summary>
+        /// Creates a new state machine of the specified <see cref="Type"/> and with the specified
+        /// optional <see cref="Event"/>. This event can only be used to access its payload,
+        /// and cannot be handled. The method returns only when the state machine is initialized and
+        /// the <see cref="Event"/> (if any) is handled.
+        /// </summary>
+        /// <param name="type">Type of the state machine.</param>
+        /// <param name="initialEvent">Optional event used during initialization.</param>
+        /// <param name="opGroupId">Optional id that can be used to identify this operation.</param>
+        /// <returns>Task that represents the asynchronous operation. The task result is the state machine id.</returns>
+        Task<StateMachineId> CreateStateMachineAndExecuteAsync(Type type, Event initialEvent = null, Guid opGroupId = default);
+
+        /// <summary>
+        /// Creates a new state machine of the specified <see cref="Type"/> and name, and with the
+        /// specified optional <see cref="Event"/>. This event can only be used to access
+        /// its payload, and cannot be handled. The method returns only when the state machine is
+        /// initialized and the <see cref="Event"/> (if any) is handled.
+        /// </summary>
+        /// <param name="type">Type of the state machine.</param>
+        /// <param name="name">Optional name used for logging.</param>
+        /// <param name="initialEvent">Optional event used during initialization.</param>
+        /// <param name="opGroupId">Optional id that can be used to identify this operation.</param>
+        /// <returns>Task that represents the asynchronous operation. The task result is the state machine id.</returns>
+        Task<StateMachineId> CreateStateMachineAndExecuteAsync(Type type, string name, Event initialEvent = null,
+            Guid opGroupId = default);
+
+        /// <summary>
+        /// Creates a new state machine of the specified <see cref="Type"/>, using the specified unbound
+        /// state machine id, and passes the specified optional <see cref="Event"/>. This event can only
+        /// be used to access its payload, and cannot be handled. The method returns only when
+        /// the state machine is initialized and the <see cref="Event"/> (if any)
+        /// is handled.
+        /// </summary>
+        /// <param name="id">Unbound state machine id.</param>
+        /// <param name="type">Type of the state machine.</param>
+        /// <param name="initialEvent">Optional event used during initialization.</param>
+        /// <param name="opGroupId">Optional id that can be used to identify this operation.</param>
+        /// <returns>Task that represents the asynchronous operation. The task result is the state machine id.</returns>
+        Task<StateMachineId> CreateStateMachineAndExecuteAsync(StateMachineId id, Type type, Event initialEvent = null,
+            Guid opGroupId = default);
+
+        /// <summary>
+        /// Sends an asynchronous <see cref="Event"/> to an state machine.
+        /// </summary>
+        /// <param name="targetId">The id of the target.</param>
+        /// <param name="e">The event to send.</param>
+        /// <param name="opGroupId">Optional id that can be used to identify this operation.</param>
+        void SendEvent(StateMachineId targetId, Event e, Guid opGroupId = default);
+
+        /// <summary>
+        /// Sends an <see cref="Event"/> to an state machine. Returns immediately if the target was already
+        /// running. Otherwise blocks until the target handles the event and reaches quiescense.
+        /// </summary>
+        /// <param name="targetId">The id of the target.</param>
+        /// <param name="e">The event to send.</param>
+        /// <param name="opGroupId">Optional id that can be used to identify this operation.</param>
+        /// <returns>Task that represents the asynchronous operation. The task result is true if
+        /// the event was handled, false if the event was only enqueued.</returns>
+        Task<bool> SendEventAndExecuteAsync(StateMachineId targetId, Event e, Guid opGroupId = default);
+
+        /// <summary>
+        /// Returns the operation group id of the state machine with the specified id. Returns <see cref="Guid.Empty"/>
+        /// if the id is not set, or if the <see cref="StateMachineId"/> is not associated with this runtime. During
+        /// testing, the runtime asserts that the specified state machine is currently executing.
+        /// </summary>
+        /// <param name="currentStateMachineId">The id of the currently executing state machine.</param>
+        /// <returns>The unique identifier.</returns>
+        Guid GetCurrentOperationGroupId(StateMachineId currentStateMachineId);
+
+        /// <summary>
+        /// Use this method to register an <see cref="IStateMachineRuntimeLog"/>.
+        /// </summary>
+        /// <param name="log">The log writer to register.</param>
+        void RegisterLog(IStateMachineRuntimeLog log);
+
+        /// <summary>
+        /// Use this method to unregister a previously registered <see cref="IStateMachineRuntimeLog"/>.
+        /// </summary>
+        /// <param name="log">The previously registered log writer to unregister.</param>
+        void RemoveLog(IStateMachineRuntimeLog log);
+    }
+}
\ No newline at end of file
diff --git a/Src/PChecker/CheckerCore/Actors/Logging/IActorRuntimeLog.cs b/Src/PChecker/CheckerCore/StateMachines/Logging/IStateMachineRuntimeLog.cs
similarity index 62%
rename from Src/PChecker/CheckerCore/Actors/Logging/IActorRuntimeLog.cs
rename to Src/PChecker/CheckerCore/StateMachines/Logging/IStateMachineRuntimeLog.cs
index ed4cb0b95..32d2b4ad1 100644
--- a/Src/PChecker/CheckerCore/Actors/Logging/IActorRuntimeLog.cs
+++ b/Src/PChecker/CheckerCore/StateMachines/Logging/IStateMachineRuntimeLog.cs
@@ -2,170 +2,162 @@
 // Licensed under the MIT License.
 
 using System;
-using PChecker.Actors.Events;
+using PChecker.StateMachines.Events;
 
-namespace PChecker.Actors.Logging
+namespace PChecker.StateMachines.Logging
 {
     /// <summary>
     /// Interface that allows an external module to track what
-    /// is happening in the <see cref="IActorRuntime"/>.
+    /// is happening in the <see cref="IStateMachineRuntime"/>.
     /// </summary>
-    public interface IActorRuntimeLog
+    public interface IStateMachineRuntimeLog
     {
-        /// <summary>
-        /// Invoked when the specified actor has been created.
-        /// </summary>
-        /// <param name="id">The id of the actor that has been created.</param>
-        /// <param name="creatorName">The name of the creator, or null.</param>
-        /// <param name="creatorType">The type of the creator, or null.</param>
-        void OnCreateActor(ActorId id, string creatorName, string creatorType);
-
         /// <summary>
         /// Invoked when the specified state machine has been created.
         /// </summary>
         /// <param name="id">The id of the state machine that has been created.</param>
         /// <param name="creatorName">The name of the creator, or null.</param>
         /// <param name="creatorType">The type of the creator, or null.</param>
-        void OnCreateStateMachine(ActorId id, string creatorName, string creatorType);
+        void OnCreateStateMachine(StateMachineId id, string creatorName, string creatorType);
 
         /// <summary>
-        /// Invoked when the specified actor executes an action.
+        /// Invoked when the specified state machine executes an action.
         /// </summary>
-        /// <param name="id">The id of the actor executing the action.</param>
+        /// <param name="id">The id of the state machine executing the action.</param>
         /// <param name="handlingStateName">The state that declared this action (can be different from currentStateName in the case of pushed states.</param>
-        /// <param name="currentStateName">The state name, if the actor is a state machine and a state exists, else null.</param>
+        /// <param name="currentStateName">The state name, if the state machine is a state machine and a state exists, else null.</param>
         /// <param name="actionName">The name of the action being executed.</param>
-        void OnExecuteAction(ActorId id, string handlingStateName, string currentStateName, string actionName);
+        void OnExecuteAction(StateMachineId id, string handlingStateName, string currentStateName, string actionName);
 
         /// <summary>
-        /// Invoked when the specified event is sent to a target actor.
+        /// Invoked when the specified event is sent to a target state machine.
         /// </summary>
-        /// <param name="targetActorId">The id of the target actor.</param>
+        /// <param name="targetStateMachineId">The id of the target state machine.</param>
         /// <param name="senderName">The name of the sender, if any.</param>
         /// <param name="senderType">The type of the sender, if any.</param>
         /// <param name="senderStateName">The state name, if the sender is a state machine, else null.</param>
         /// <param name="e">The event being sent.</param>
         /// <param name="opGroupId">The id used to identify the send operation.</param>
-        /// <param name="isTargetHalted">Is the target actor halted.</param>
-        void OnSendEvent(ActorId targetActorId, string senderName, string senderType, string senderStateName,
+        /// <param name="isTargetHalted">Is the target state machine halted.</param>
+        void OnSendEvent(StateMachineId targetStateMachineId, string senderName, string senderType, string senderStateName,
             Event e, Guid opGroupId, bool isTargetHalted);
 
         /// <summary>
         /// Invoked when the specified state machine raises an event.
         /// </summary>
-        /// <param name="id">The id of the actor raising the event.</param>
+        /// <param name="id">The id of the state machine raising the event.</param>
         /// <param name="stateName">The name of the current state.</param>
         /// <param name="e">The event being raised.</param>
-        void OnRaiseEvent(ActorId id, string stateName, Event e);
+        void OnRaiseEvent(StateMachineId id, string stateName, Event e);
 
         /// <summary>
-        /// Invoked when the specified event is about to be enqueued to an actor.
+        /// Invoked when the specified event is about to be enqueued to an state machine.
         /// </summary>
-        /// <param name="id">The id of the actor that the event is being enqueued to.</param>
+        /// <param name="id">The id of the state machine that the event is being enqueued to.</param>
         /// <param name="e">The event being enqueued.</param>
-        void OnEnqueueEvent(ActorId id, Event e);
+        void OnEnqueueEvent(StateMachineId id, Event e);
 
         /// <summary>
-        /// Invoked when the specified event is dequeued by an actor.
+        /// Invoked when the specified event is dequeued by an state machine.
         /// </summary>
-        /// <param name="id">The id of the actor that the event is being dequeued by.</param>
-        /// <param name="stateName">The state name, if the actor is a state machine and a state exists, else null.</param>
+        /// <param name="id">The id of the state machine that the event is being dequeued by.</param>
+        /// <param name="stateName">The state name, if the state machine is a state machine and a state exists, else null.</param>
         /// <param name="e">The event being dequeued.</param>
-        void OnDequeueEvent(ActorId id, string stateName, Event e);
+        void OnDequeueEvent(StateMachineId id, string stateName, Event e);
 
         /// <summary>
-        /// Invoked when the specified event is received by an actor.
+        /// Invoked when the specified event is received by an state machine.
         /// </summary>
-        /// <param name="id">The id of the actor that received the event.</param>
-        /// <param name="stateName">The state name, if the actor is a state machine and a state exists, else null.</param>
+        /// <param name="id">The id of the state machine that received the event.</param>
+        /// <param name="stateName">The state name, if the state machine is a state machine and a state exists, else null.</param>
         /// <param name="e">The the event being received.</param>
-        /// <param name="wasBlocked">The actor was waiting for one or more specific events,
+        /// <param name="wasBlocked">The state machine was waiting for one or more specific events,
         /// and <paramref name="e"/> was one of them</param>
-        void OnReceiveEvent(ActorId id, string stateName, Event e, bool wasBlocked);
+        void OnReceiveEvent(StateMachineId id, string stateName, Event e, bool wasBlocked);
 
         /// <summary>
-        /// Invoked when the specified actor waits to receive an event of a specified type.
+        /// Invoked when the specified state machine waits to receive an event of a specified type.
         /// </summary>
-        /// <param name="id">The id of the actor that is entering the wait state.</param>
-        /// <param name="stateName">The state name, if the actor is a state machine and a state exists, else null.</param>
+        /// <param name="id">The id of the state machine that is entering the wait state.</param>
+        /// <param name="stateName">The state name, if the state machine is a state machine and a state exists, else null.</param>
         /// <param name="eventType">The type of the event being waited for.</param>
-        void OnWaitEvent(ActorId id, string stateName, Type eventType);
+        void OnWaitEvent(StateMachineId id, string stateName, Type eventType);
 
         /// <summary>
-        /// Invoked when the specified actor waits to receive an event of one of the specified types.
+        /// Invoked when the specified state machine waits to receive an event of one of the specified types.
         /// </summary>
-        /// <param name="id">The id of the actor that is entering the wait state.</param>
-        /// <param name="stateName">The state name, if the actor is a state machine and a state exists, else null.</param>
+        /// <param name="id">The id of the state machine that is entering the wait state.</param>
+        /// <param name="stateName">The state name, if the state machine is a state machine and a state exists, else null.</param>
         /// <param name="eventTypes">The types of the events being waited for, if any.</param>
-        void OnWaitEvent(ActorId id, string stateName, params Type[] eventTypes);
+        void OnWaitEvent(StateMachineId id, string stateName, params Type[] eventTypes);
 
         /// <summary>
         /// Invoked when the specified state machine enters or exits a state.
         /// </summary>
-        /// <param name="id">The id of the actor entering or exiting the state.</param>
+        /// <param name="id">The id of the state machine entering or exiting the state.</param>
         /// <param name="stateName">The name of the state being entered or exited.</param>
         /// <param name="isEntry">If true, this is called for a state entry; otherwise, exit.</param>
-        void OnStateTransition(ActorId id, string stateName, bool isEntry);
+        void OnStateTransition(StateMachineId id, string stateName, bool isEntry);
 
         /// <summary>
         /// Invoked when the specified state machine performs a goto transition to the specified state.
         /// </summary>
-        /// <param name="id">The id of the actor.</param>
+        /// <param name="id">The id of the state machine.</param>
         /// <param name="currentStateName">The name of the current state.</param>
         /// <param name="newStateName">The target state of the transition.</param>
-        void OnGotoState(ActorId id, string currentStateName, string newStateName);
+        void OnGotoState(StateMachineId id, string currentStateName, string newStateName);
 
 
         /// <summary>
-        /// Invoked when the specified actor is idle (there is nothing to dequeue) and the default
+        /// Invoked when the specified state machine is idle (there is nothing to dequeue) and the default
         /// event handler is about to be executed.
         /// </summary>
-        /// <param name="id">The id of the actor that the state will execute in.</param>
-        /// <param name="stateName">The state name, if the actor is a state machine and a state exists, else null.</param>
-        void OnDefaultEventHandler(ActorId id, string stateName);
+        /// <param name="id">The id of the state machine that the state will execute in.</param>
+        /// <param name="stateName">The state name, if the state machine is a state machine and a state exists, else null.</param>
+        void OnDefaultEventHandler(StateMachineId id, string stateName);
 
         /// <summary>
-        /// Invoked when the specified actor has been halted.
+        /// Invoked when the specified state machine has been halted.
         /// </summary>
-        /// <param name="id">The id of the actor that has been halted.</param>
+        /// <param name="id">The id of the state machine that has been halted.</param>
         /// <param name="inboxSize">Approximate size of the inbox.</param>
-        void OnHalt(ActorId id, int inboxSize);
+        void OnHalt(StateMachineId id, int inboxSize);
 
         /// <summary>
-        /// Invoked when the specified actor handled a raised event.
+        /// Invoked when the specified state machine handled a raised event.
         /// </summary>
-        /// <param name="id">The id of the actor handling the event.</param>
-        /// <param name="stateName">The state name, if the actor is a state machine and a state exists, else null.</param>
+        /// <param name="id">The id of the state machine handling the event.</param>
+        /// <param name="stateName">The state name, if the state machine is a state machine and a state exists, else null.</param>
         /// <param name="e">The event being handled.</param>
-        void OnHandleRaisedEvent(ActorId id, string stateName, Event e);
+        void OnHandleRaisedEvent(StateMachineId id, string stateName, Event e);
 
         /// <summary>
         /// Invoked when the specified event cannot be handled in the current state, its exit
         /// handler is executed and then the state is popped and any previous "current state"
         /// is reentered. This handler is called when that pop has been done.
         /// </summary>
-        /// <param name="id">The id of the actor that the pop executed in.</param>
-        /// <param name="stateName">The state name, if the actor is a state machine and a state exists, else null.</param>
+        /// <param name="id">The id of the state machine that the pop executed in.</param>
+        /// <param name="stateName">The state name, if the state machine is a state machine and a state exists, else null.</param>
         /// <param name="e">The event that cannot be handled.</param>
-        void OnPopStateUnhandledEvent(ActorId id, string stateName, Event e);
+        void OnPopStateUnhandledEvent(StateMachineId id, string stateName, Event e);
 
         /// <summary>
-        /// Invoked when the specified actor throws an exception.
+        /// Invoked when the specified state machine throws an exception.
         /// </summary>
-        /// <param name="id">The id of the actor that threw the exception.</param>
-        /// <param name="stateName">The state name, if the actor is a state machine and a state exists, else null.</param>
+        /// <param name="id">The id of the state machine that threw the exception.</param>
+        /// <param name="stateName">The state name, if the state machine is a state machine and a state exists, else null.</param>
         /// <param name="actionName">The name of the action being executed.</param>
         /// <param name="ex">The exception.</param>
-        void OnExceptionThrown(ActorId id, string stateName, string actionName, Exception ex);
+        void OnExceptionThrown(StateMachineId id, string stateName, string actionName, Exception ex);
 
         /// <summary>
         /// Invoked when the specified OnException method is used to handle a thrown exception.
         /// </summary>
-        /// <param name="id">The id of the actor that threw the exception.</param>
-        /// <param name="stateName">The state name, if the actor is a state machine and a state exists, else null.</param>
+        /// <param name="id">The id of the state machine that threw the exception.</param>
+        /// <param name="stateName">The state name, if the state machine is a state machine and a state exists, else null.</param>
         /// <param name="actionName">The name of the action being executed.</param>
         /// <param name="ex">The exception.</param>
-        void OnExceptionHandled(ActorId id, string stateName, string actionName, Exception ex);
+        void OnExceptionHandled(StateMachineId id, string stateName, string actionName, Exception ex);
 
 
         /// <summary>
diff --git a/Src/PChecker/CheckerCore/Actors/Logging/JsonWriter.cs b/Src/PChecker/CheckerCore/StateMachines/Logging/JsonWriter.cs
similarity index 96%
rename from Src/PChecker/CheckerCore/Actors/Logging/JsonWriter.cs
rename to Src/PChecker/CheckerCore/StateMachines/Logging/JsonWriter.cs
index d315d1cd7..15c950fc3 100644
--- a/Src/PChecker/CheckerCore/Actors/Logging/JsonWriter.cs
+++ b/Src/PChecker/CheckerCore/StateMachines/Logging/JsonWriter.cs
@@ -6,7 +6,7 @@
 using System.Security.Cryptography;
 using System.Text;
 
-namespace PChecker.Actors.Logging
+namespace PChecker.StateMachines.Logging
 {
     /// <summary>
     /// Class for handling generating the vector clock for a log entry
@@ -349,9 +349,9 @@ public LogEntry()
     /// Enum representing the possible attributes in the details dictionary,
     /// which represents the data associated with a specific log type. All of
     /// the following are available or expanded parameters associated with an
-    /// IActorRuntime method. Naming for them is mostly the same except some
+    /// IStateMachineRuntime method. Naming for them is mostly the same except some
     /// are changed for simplicity.
-    /// I.e., for OnRaiseEvent(ActorId id, string, stateName, Event e), it
+    /// I.e., for OnRaiseEvent(StateMachineId id, string, stateName, Event e), it
     /// will have attributes id, state (simplified from stateName, event
     /// (simplified from eventName within Event e), and payload (in Event e).
     /// </summary>
@@ -365,7 +365,7 @@ public class LogDetails
         public string? Log { get; set; }
 
         /// <summary>
-        /// The actor id.
+        /// The state machine id.
         /// </summary>
         public string? Id { get; set; }
 
@@ -437,7 +437,7 @@ public class LogDetails
         public int? HaltInboxSize { get; set; }
 
         /// <summary>
-        /// Boolean representing whether an actor was waiting for one or more events
+        /// Boolean representing whether an state machine was waiting for one or more events
         /// Available for log type ReceiveEvent.
         /// </summary>
         public bool? WasBlocked { get; set; }
@@ -449,7 +449,7 @@ public class LogDetails
         public string? Sender { get; set; }
 
         /// <summary>
-        /// Id of target actor.
+        /// Id of target state machine.
         /// Available for log type SendEvent.
         /// </summary>
         public string? Target { get; set; }
@@ -461,7 +461,7 @@ public class LogDetails
         public string? OpGroupId { get; set; }
 
         /// <summary>
-        /// Boolean representing whether the target actor was halted.
+        /// Boolean representing whether the target state machine was halted.
         /// Available for log type SendEvent.
         /// </summary>
         public bool? IsTargetHalted { get; set; }
@@ -558,7 +558,7 @@ public JsonWriter()
         /// <summary>
         /// Enum representing the different log types the JSON error trace logs.
         /// Referenced from PLogFormatter.cs and PCheckerLogTextFormatter.cs
-        /// to see what those formatter logs. Check IActorRuntimeLog.cs to see
+        /// to see what those formatter logs. Check IStateMachineRuntimeLog.cs to see
         /// each log types' description and when they are invoked.
         /// </summary>
         public enum LogType
@@ -568,11 +568,6 @@ public enum LogType
             /// </summary>
             AssertionFailure,
 
-            /// <summary>
-            /// Invoked when the specified actor has been created.
-            /// </summary>
-            CreateActor,
-
             /// <summary>
             /// Invoked when the specified state machine has been created.
             /// </summary>
@@ -584,13 +579,13 @@ public enum LogType
             CreateMonitor,
 
             /// <summary>
-            /// Invoked when the specified actor is idle (there is nothing to dequeue) and the default
+            /// Invoked when the specified state machine is idle (there is nothing to dequeue) and the default
             /// event handler is about to be executed.
             /// </summary>
             DefaultEventHandler,
 
             /// <summary>
-            /// Invoked when the specified event is dequeued by an actor.
+            /// Invoked when the specified event is dequeued by an state machine.
             /// </summary>
             DequeueEvent,
 
@@ -600,7 +595,7 @@ public enum LogType
             ExceptionHandled,
 
             /// <summary>
-            /// Invoked when the specified actor throws an exception.
+            /// Invoked when the specified state machine throws an exception.
             /// </summary>
             ExceptionThrown,
 
@@ -610,7 +605,7 @@ public enum LogType
             GotoState,
 
             /// <summary>
-            /// Invoked when the specified actor has been halted.
+            /// Invoked when the specified state machine has been halted.
             /// </summary>
             Halt,
 
@@ -652,12 +647,12 @@ public enum LogType
             RaiseEvent,
 
             /// <summary>
-            /// Invoked when the specified event is received by an actor.
+            /// Invoked when the specified event is received by an state machine.
             /// </summary>
             ReceiveEvent,
 
             /// <summary>
-            /// Invoked when the specified event is sent to a target actor.
+            /// Invoked when the specified event is sent to a target state machine.
             /// </summary>
             SendEvent,
 
@@ -672,12 +667,12 @@ public enum LogType
             StrategyDescription,
 
             /// <summary>
-            /// Invoked when the specified actor waits to receive an event of a specified type.
+            /// Invoked when the specified state machine waits to receive an event of a specified type.
             /// </summary>
             WaitEvent,
 
             /// <summary>
-            /// Invoked when the specified actor waits to receive multiple events of a specified type.
+            /// Invoked when the specified state machine waits to receive multiple events of a specified type.
             /// </summary>
             WaitMultipleEvents,
 
diff --git a/Src/PChecker/CheckerCore/Actors/Logging/LogWriter.cs b/Src/PChecker/CheckerCore/StateMachines/Logging/LogWriter.cs
similarity index 75%
rename from Src/PChecker/CheckerCore/Actors/Logging/LogWriter.cs
rename to Src/PChecker/CheckerCore/StateMachines/Logging/LogWriter.cs
index c991b1378..70d4ddad6 100644
--- a/Src/PChecker/CheckerCore/Actors/Logging/LogWriter.cs
+++ b/Src/PChecker/CheckerCore/StateMachines/Logging/LogWriter.cs
@@ -5,21 +5,21 @@
 using System.Collections.Generic;
 using System.IO;
 using System.Linq;
-using PChecker.Actors.Events;
+using PChecker.StateMachines.Events;
 using PChecker.IO.Logging;
 
-namespace PChecker.Actors.Logging
+namespace PChecker.StateMachines.Logging
 {
     /// <summary>
     /// Manages the installed <see cref="TextWriter"/> and all registered
-    /// <see cref="IActorRuntimeLog"/> objects.
+    /// <see cref="IStateMachineRuntimeLog"/> objects.
     /// </summary>
     internal sealed class LogWriter
     {
         /// <summary>
         /// The set of registered log writers.
         /// </summary>
-        private readonly HashSet<IActorRuntimeLog> Logs;
+        private readonly HashSet<IStateMachineRuntimeLog> Logs;
 
         /// <summary>
         /// Used to log messages.
@@ -36,7 +36,7 @@ internal sealed class LogWriter
         /// </summary>
         internal LogWriter(CheckerConfiguration checkerConfiguration)
         {
-            Logs = new HashSet<IActorRuntimeLog>();
+            Logs = new HashSet<IStateMachineRuntimeLog>();
 
             if (checkerConfiguration.IsVerbose)
             {
@@ -48,30 +48,13 @@ internal LogWriter(CheckerConfiguration checkerConfiguration)
             }
         }
 
-        /// <summary>
-        /// Logs that the specified actor has been created.
-        /// </summary>
-        /// <param name="id">The id of the actor that has been created.</param>
-        /// <param name="creatorName">The name of the creator, or null.</param>
-        /// <param name="creatorType">The type of the creator, or null.</param>
-        public void LogCreateActor(ActorId id, string creatorName, string creatorType)
-        {
-            if (Logs.Count > 0)
-            {
-                foreach (var log in Logs)
-                {
-                    log.OnCreateActor(id, creatorName, creatorType);
-                }
-            }
-        }
-
         /// <summary>
         /// Logs that the specified state machine has been created.
         /// </summary>
         /// <param name="id">The id of the state machine that has been created.</param>
         /// <param name="creatorName">The name of the creator, or null.</param>
         /// <param name="creatorType">The type of the creator, or null.</param>
-        public void LogCreateStateMachine(ActorId id, string creatorName, string creatorType)
+        public void LogCreateStateMachine(StateMachineId id, string creatorName, string creatorType)
         {
             if (Logs.Count > 0)
             {
@@ -83,13 +66,13 @@ public void LogCreateStateMachine(ActorId id, string creatorName, string creator
         }
 
         /// <summary>
-        /// Logs that the specified actor executes an action.
+        /// Logs that the specified state machine executes an action.
         /// </summary>
-        /// <param name="id">The id of the actor executing the action.</param>
+        /// <param name="id">The id of the state machine executing the action.</param>
         /// <param name="handlingStateName">The state that declared this action (can be different from currentStateName in the case of PushStates.</param>
-        /// <param name="currentStateName">The state name, if the actor is a state machine and a state exists, else null.</param>
+        /// <param name="currentStateName">The state name, if the state machine is a state machine and a state exists, else null.</param>
         /// <param name="actionName">The name of the action being executed.</param>
-        public void LogExecuteAction(ActorId id, string handlingStateName, string currentStateName, string actionName)
+        public void LogExecuteAction(StateMachineId id, string handlingStateName, string currentStateName, string actionName)
         {
             if (Logs.Count > 0)
             {
@@ -101,34 +84,34 @@ public void LogExecuteAction(ActorId id, string handlingStateName, string curren
         }
 
         /// <summary>
-        /// Logs that the specified event is sent to a target actor.
+        /// Logs that the specified event is sent to a target state machine.
         /// </summary>
-        /// <param name="targetActorId">The id of the target actor.</param>
+        /// <param name="targetStateMachineId">The id of the target state machine.</param>
         /// <param name="senderName">The name of the sender, if any.</param>
         /// <param name="senderType">The type of the sender, if any.</param>
         /// <param name="senderState">The state name, if the sender is a state machine, else null.</param>
         /// <param name="e">The event being sent.</param>
         /// <param name="opGroupId">The id used to identify the send operation.</param>
-        /// <param name="isTargetHalted">Is the target actor halted.</param>
-        public void LogSendEvent(ActorId targetActorId, string senderName, string senderType, string senderState,
+        /// <param name="isTargetHalted">Is the target state machine halted.</param>
+        public void LogSendEvent(StateMachineId targetStateMachineId, string senderName, string senderType, string senderState,
             Event e, Guid opGroupId, bool isTargetHalted)
         {
             if (Logs.Count > 0)
             {
                 foreach (var log in Logs)
                 {
-                    log.OnSendEvent(targetActorId, senderName, senderType, senderState, e, opGroupId, isTargetHalted);
+                    log.OnSendEvent(targetStateMachineId, senderName, senderType, senderState, e, opGroupId, isTargetHalted);
                 }
             }
         }
 
         /// <summary>
-        /// Logs that the specified actor raises an event.
+        /// Logs that the specified state machine raises an event.
         /// </summary>
-        /// <param name="id">The id of the actor raising the event.</param>
-        /// <param name="stateName">The state name, if the actor is a state machine and a state exists, else null.</param>
+        /// <param name="id">The id of the state machine raising the event.</param>
+        /// <param name="stateName">The state name, if the state machine is a state machine and a state exists, else null.</param>
         /// <param name="e">The event being raised.</param>
-        public void LogRaiseEvent(ActorId id, string stateName, Event e)
+        public void LogRaiseEvent(StateMachineId id, string stateName, Event e)
         {
             if (Logs.Count > 0)
             {
@@ -140,11 +123,11 @@ public void LogRaiseEvent(ActorId id, string stateName, Event e)
         }
 
         /// <summary>
-        /// Logs that the specified event is about to be enqueued to an actor.
+        /// Logs that the specified event is about to be enqueued to an state machine.
         /// </summary>
-        /// <param name="id">The id of the actor that the event is being enqueued to.</param>
+        /// <param name="id">The id of the state machine that the event is being enqueued to.</param>
         /// <param name="e">The event being enqueued.</param>
-        public void LogEnqueueEvent(ActorId id, Event e)
+        public void LogEnqueueEvent(StateMachineId id, Event e)
         {
             if (Logs.Count > 0)
             {
@@ -156,12 +139,12 @@ public void LogEnqueueEvent(ActorId id, Event e)
         }
 
         /// <summary>
-        /// Logs that the specified event is dequeued by an actor.
+        /// Logs that the specified event is dequeued by an state machine.
         /// </summary>
-        /// <param name="id">The id of the actor that the event is being dequeued by.</param>
-        /// <param name="stateName">The state name, if the actor is a state machine and a state exists, else null.</param>
+        /// <param name="id">The id of the state machine that the event is being dequeued by.</param>
+        /// <param name="stateName">The state name, if the state machine is a state machine and a state exists, else null.</param>
         /// <param name="e">The event being dequeued.</param>
-        public void LogDequeueEvent(ActorId id, string stateName, Event e)
+        public void LogDequeueEvent(StateMachineId id, string stateName, Event e)
         {
             if (Logs.Count > 0)
             {
@@ -173,14 +156,14 @@ public void LogDequeueEvent(ActorId id, string stateName, Event e)
         }
 
         /// <summary>
-        /// Logs that the specified event is received by an actor.
+        /// Logs that the specified event is received by an state machine.
         /// </summary>
-        /// <param name="id">The id of the actor that received the event.</param>
-        /// <param name="stateName">The state name, if the actor is a state machine and a state exists, else null.</param>
+        /// <param name="id">The id of the state machine that received the event.</param>
+        /// <param name="stateName">The state name, if the state machine is a state machine and a state exists, else null.</param>
         /// <param name="e">The event being received.</param>
         /// <param name="wasBlocked">The state machine was waiting for one or more specific events,
         /// and <paramref name="e"/> was one of them.</param>
-        public void LogReceiveEvent(ActorId id, string stateName, Event e, bool wasBlocked)
+        public void LogReceiveEvent(StateMachineId id, string stateName, Event e, bool wasBlocked)
         {
             if (Logs.Count > 0)
             {
@@ -192,12 +175,12 @@ public void LogReceiveEvent(ActorId id, string stateName, Event e, bool wasBlock
         }
 
         /// <summary>
-        /// Logs that the specified actor waits to receive an event of a specified type.
+        /// Logs that the specified state machine waits to receive an event of a specified type.
         /// </summary>
-        /// <param name="id">The id of the actor that is entering the wait state.</param>
-        /// <param name="stateName">The state name, if the actor is a state machine and a state exists, else null.</param>
+        /// <param name="id">The id of the state machine that is entering the wait state.</param>
+        /// <param name="stateName">The state name, if the state machine is a state machine and a state exists, else null.</param>
         /// <param name="eventType">The type of the event being waited for.</param>
-        public void LogWaitEvent(ActorId id, string stateName, Type eventType)
+        public void LogWaitEvent(StateMachineId id, string stateName, Type eventType)
         {
             if (Logs.Count > 0)
             {
@@ -209,12 +192,12 @@ public void LogWaitEvent(ActorId id, string stateName, Type eventType)
         }
 
         /// <summary>
-        /// Logs that the specified actor waits to receive an event of one of the specified types.
+        /// Logs that the specified state machine waits to receive an event of one of the specified types.
         /// </summary>
-        /// <param name="id">The id of the actor that is entering the wait state.</param>
-        /// <param name="stateName">The state name, if the actor is a state machine and a state exists, else null.</param>
+        /// <param name="id">The id of the state machine that is entering the wait state.</param>
+        /// <param name="stateName">The state name, if the state machine is a state machine and a state exists, else null.</param>
         /// <param name="eventTypes">The types of the events being waited for, if any.</param>
-        public void LogWaitEvent(ActorId id, string stateName, params Type[] eventTypes)
+        public void LogWaitEvent(StateMachineId id, string stateName, params Type[] eventTypes)
         {
             if (Logs.Count > 0)
             {
@@ -245,10 +228,10 @@ public void LogRandom(object result, string callerName, string callerType)
         /// <summary>
         /// Logs that the specified state machine enters or exits a state.
         /// </summary>
-        /// <param name="id">The id of the actor entering or exiting the state.</param>
+        /// <param name="id">The id of the state machine entering or exiting the state.</param>
         /// <param name="stateName">The name of the state being entered or exited.</param>
         /// <param name="isEntry">If true, this is called for a state entry; otherwise, exit.</param>
-        public void LogStateTransition(ActorId id, string stateName, bool isEntry)
+        public void LogStateTransition(StateMachineId id, string stateName, bool isEntry)
         {
             if (Logs.Count > 0)
             {
@@ -262,10 +245,10 @@ public void LogStateTransition(ActorId id, string stateName, bool isEntry)
         /// <summary>
         /// Logs that the specified state machine performs a goto state transition.
         /// </summary>
-        /// <param name="id">The id of the actor.</param>
+        /// <param name="id">The id of the state machine.</param>
         /// <param name="currentStateName">The name of the current state.</param>
         /// <param name="newStateName">The target state of the transition.</param>
-        public void LogGotoState(ActorId id, string currentStateName, string newStateName)
+        public void LogGotoState(StateMachineId id, string currentStateName, string newStateName)
         {
             if (Logs.Count > 0)
             {
@@ -277,11 +260,11 @@ public void LogGotoState(ActorId id, string currentStateName, string newStateNam
         }
 
         /// <summary>
-        /// Logs that the specified actor has halted.
+        /// Logs that the specified state machine has halted.
         /// </summary>
-        /// <param name="id">The id of the actor that has been halted.</param>
+        /// <param name="id">The id of the state machine that has been halted.</param>
         /// <param name="inboxSize">Approximate size of the inbox.</param>
-        public void LogHalt(ActorId id, int inboxSize)
+        public void LogHalt(StateMachineId id, int inboxSize)
         {
             if (Logs.Count > 0)
             {
@@ -293,12 +276,12 @@ public void LogHalt(ActorId id, int inboxSize)
         }
 
         /// <summary>
-        /// Logs that the specified actor is idle (there is nothing to dequeue) and the default
+        /// Logs that the specified state machine is idle (there is nothing to dequeue) and the default
         /// event handler is about to be executed.
         /// </summary>
-        /// <param name="id">The id of the actor that the state will execute in.</param>
-        /// <param name="stateName">The state name, if the actor is a state machine and a state exists, else null.</param>
-        public void LogDefaultEventHandler(ActorId id, string stateName)
+        /// <param name="id">The id of the state machine that the state will execute in.</param>
+        /// <param name="stateName">The state name, if the state machine is a state machine and a state exists, else null.</param>
+        public void LogDefaultEventHandler(StateMachineId id, string stateName)
         {
             if (Logs.Count > 0)
             {
@@ -312,10 +295,10 @@ public void LogDefaultEventHandler(ActorId id, string stateName)
         /// <summary>
         /// Logs that the specified state machine handled a raised event.
         /// </summary>
-        /// <param name="id">The id of the actor handling the event.</param>
+        /// <param name="id">The id of the state machine handling the event.</param>
         /// <param name="stateName">The name of the current state.</param>
         /// <param name="e">The event being handled.</param>
-        public void LogHandleRaisedEvent(ActorId id, string stateName, Event e)
+        public void LogHandleRaisedEvent(StateMachineId id, string stateName, Event e)
         {
             if (Logs.Count > 0)
             {
@@ -331,10 +314,10 @@ public void LogHandleRaisedEvent(ActorId id, string stateName, Event e)
         /// handler is executed and then the state is popped and any previous "current state"
         /// is reentered. This handler is called when that pop has been done.
         /// </summary>
-        /// <param name="id">The id of the actor that the pop executed in.</param>
-        /// <param name="stateName">The state name, if the actor is a state machine and a state exists, else null.</param>
+        /// <param name="id">The id of the state machine that the pop executed in.</param>
+        /// <param name="stateName">The state name, if the state machine is a state machine and a state exists, else null.</param>
         /// <param name="e">The event that cannot be handled.</param>
-        public void LogPopStateUnhandledEvent(ActorId id, string stateName, Event e)
+        public void LogPopStateUnhandledEvent(StateMachineId id, string stateName, Event e)
         {
             if (Logs.Count > 0)
             {
@@ -346,13 +329,13 @@ public void LogPopStateUnhandledEvent(ActorId id, string stateName, Event e)
         }
 
         /// <summary>
-        /// Logs that the specified actor throws an exception.
+        /// Logs that the specified state machine throws an exception.
         /// </summary>
-        /// <param name="id">The id of the actor that threw the exception.</param>
-        /// <param name="stateName">The state name, if the actor is a state machine and a state exists, else null.</param>
+        /// <param name="id">The id of the state machine that threw the exception.</param>
+        /// <param name="stateName">The state name, if the state machine is a state machine and a state exists, else null.</param>
         /// <param name="actionName">The name of the action being executed.</param>
         /// <param name="ex">The exception.</param>
-        public void LogExceptionThrown(ActorId id, string stateName, string actionName, Exception ex)
+        public void LogExceptionThrown(StateMachineId id, string stateName, string actionName, Exception ex)
         {
             if (Logs.Count > 0)
             {
@@ -366,11 +349,11 @@ public void LogExceptionThrown(ActorId id, string stateName, string actionName,
         /// <summary>
         /// Logs that the specified OnException method is used to handle a thrown exception.
         /// </summary>
-        /// <param name="id">The id of the actor that threw the exception.</param>
-        /// <param name="stateName">The state name, if the actor is a state machine and a state exists, else null.</param>
+        /// <param name="id">The id of the state machine that threw the exception.</param>
+        /// <param name="stateName">The state name, if the state machine is a state machine and a state exists, else null.</param>
         /// <param name="actionName">The name of the action being executed.</param>
         /// <param name="ex">The exception.</param>
-        public void LogExceptionHandled(ActorId id, string stateName, string actionName, Exception ex)
+        public void LogExceptionHandled(StateMachineId id, string stateName, string actionName, Exception ex)
         {
             if (Logs.Count > 0)
             {
@@ -532,12 +515,12 @@ internal void LogCompletion()
         }
 
         /// <summary>
-        /// Returns all registered logs of type <typeparamref name="TActorRuntimeLog"/>,
+        /// Returns all registered logs of type <typeparamref name="TStateMachineRuntimeLog"/>,
         /// if there are any.
         /// </summary>
-        public IEnumerable<TActorRuntimeLog> GetLogsOfType<TActorRuntimeLog>()
-            where TActorRuntimeLog : IActorRuntimeLog =>
-            Logs.OfType<TActorRuntimeLog>();
+        public IEnumerable<TStateMachineRuntimeLog> GetLogsOfType<TStateMachineRuntimeLog>()
+            where TStateMachineRuntimeLog : IStateMachineRuntimeLog =>
+            Logs.OfType<TStateMachineRuntimeLog>();
 
         /// <summary>
         /// Use this method to override the default <see cref="TextWriter"/> for logging messages.
@@ -595,9 +578,9 @@ private PCheckerLogTextFormatter GetOrCreateTextLog()
         }
 
         /// <summary>
-        /// Use this method to register an <see cref="IActorRuntimeLog"/>.
+        /// Use this method to register an <see cref="IStateMachineRuntimeLog"/>.
         /// </summary>
-        internal void RegisterLog(IActorRuntimeLog log)
+        internal void RegisterLog(IStateMachineRuntimeLog log)
         {
             if (log == null)
             {
@@ -630,9 +613,9 @@ internal void RegisterLog(IActorRuntimeLog log)
         }
 
         /// <summary>
-        /// Use this method to unregister a previously registered <see cref="IActorRuntimeLog"/>.
+        /// Use this method to unregister a previously registered <see cref="IStateMachineRuntimeLog"/>.
         /// </summary>
-        internal void RemoveLog(IActorRuntimeLog log)
+        internal void RemoveLog(IStateMachineRuntimeLog log)
         {
             if (log != null)
             {
diff --git a/Src/PChecker/CheckerCore/Actors/Logging/PCheckerLogJsonFormatter.cs b/Src/PChecker/CheckerCore/StateMachines/Logging/PCheckerLogJsonFormatter.cs
similarity index 58%
rename from Src/PChecker/CheckerCore/Actors/Logging/PCheckerLogJsonFormatter.cs
rename to Src/PChecker/CheckerCore/StateMachines/Logging/PCheckerLogJsonFormatter.cs
index a76928a44..07d7b1f83 100644
--- a/Src/PChecker/CheckerCore/Actors/Logging/PCheckerLogJsonFormatter.cs
+++ b/Src/PChecker/CheckerCore/StateMachines/Logging/PCheckerLogJsonFormatter.cs
@@ -2,14 +2,14 @@
 // Licensed under the MIT License.
 
 using System;
-using PChecker.Actors.Events;
+using PChecker.StateMachines.Events;
 
-namespace PChecker.Actors.Logging
+namespace PChecker.StateMachines.Logging
 {
     /// <summary>
-    /// This class implements IActorRuntimeLog and generates log output in an XML format.
+    /// This class implements IStateMachineRuntimeLog and generates log output in an XML format.
     /// </summary>
-    public class PCheckerLogJsonFormatter : IActorRuntimeLog
+    public class PCheckerLogJsonFormatter : IStateMachineRuntimeLog
     {
         /// <summary>
         /// Get or set the JsonWriter to write to.
@@ -33,107 +33,102 @@ public virtual void OnCompleted()
         public virtual void OnAssertionFailure(string error)
         {
         }
-
-        /// <inheritdoc />
-        public virtual void OnCreateActor(ActorId id, string creatorName, string creatorType)
-        {
-        }
-
+        
         /// <inheritdoc />
-        public virtual void OnCreateStateMachine(ActorId id, string creatorName, string creatorType)
+        public virtual void OnCreateStateMachine(StateMachineId id, string creatorName, string creatorType)
         {
         }
 
         /// <inheritdoc />
-        public virtual void OnDefaultEventHandler(ActorId id, string stateName)
+        public virtual void OnDefaultEventHandler(StateMachineId id, string stateName)
         {
         }
 
         /// <inheritdoc />
-        public virtual void OnDequeueEvent(ActorId id, string stateName, Event e)
+        public virtual void OnDequeueEvent(StateMachineId id, string stateName, Event e)
         {
         }
 
         /// <inheritdoc />
-        public virtual void OnEnqueueEvent(ActorId id, Event e)
+        public virtual void OnEnqueueEvent(StateMachineId id, Event e)
         {
         }
 
         /// <inheritdoc />
-        public virtual void OnExceptionHandled(ActorId id, string stateName, string actionName, Exception ex)
+        public virtual void OnExceptionHandled(StateMachineId id, string stateName, string actionName, Exception ex)
         {
         }
 
         /// <inheritdoc />
-        public virtual void OnExceptionThrown(ActorId id, string stateName, string actionName, Exception ex)
+        public virtual void OnExceptionThrown(StateMachineId id, string stateName, string actionName, Exception ex)
         {
         }
 
         /// <inheritdoc />
-        public virtual void OnExecuteAction(ActorId id, string handlingStateName, string currentStateName,
+        public virtual void OnExecuteAction(StateMachineId id, string handlingStateName, string currentStateName,
             string actionName)
         {
         }
 
         /// <inheritdoc />
-        public virtual void OnGotoState(ActorId id, string currentStateName, string newStateName)
+        public virtual void OnGotoState(StateMachineId id, string currentStateName, string newStateName)
         {
         }
 
         /// <inheritdoc />
-        public virtual void OnHalt(ActorId id, int inboxSize)
+        public virtual void OnHalt(StateMachineId id, int inboxSize)
         {
         }
 
         /// <inheritdoc />
-        public virtual void OnHandleRaisedEvent(ActorId id, string stateName, Event e)
+        public virtual void OnHandleRaisedEvent(StateMachineId id, string stateName, Event e)
         {
         }
 
         /// <inheritdoc />
-        public virtual void OnPopState(ActorId id, string currentStateName, string restoredStateName)
+        public virtual void OnPopState(StateMachineId id, string currentStateName, string restoredStateName)
         {
         }
 
         /// <inheritdoc />
-        public virtual void OnPopStateUnhandledEvent(ActorId id, string stateName, Event e)
+        public virtual void OnPopStateUnhandledEvent(StateMachineId id, string stateName, Event e)
         {
         }
 
         /// <inheritdoc />
-        public virtual void OnPushState(ActorId id, string currentStateName, string newStateName)
+        public virtual void OnPushState(StateMachineId id, string currentStateName, string newStateName)
         {
         }
 
         /// <inheritdoc />
-        public virtual void OnRaiseEvent(ActorId id, string stateName, Event e)
+        public virtual void OnRaiseEvent(StateMachineId id, string stateName, Event e)
         {
         }
 
         /// <inheritdoc />
-        public virtual void OnReceiveEvent(ActorId id, string stateName, Event e, bool wasBlocked)
+        public virtual void OnReceiveEvent(StateMachineId id, string stateName, Event e, bool wasBlocked)
         {
         }
 
         /// <inheritdoc />
-        public virtual void OnSendEvent(ActorId targetActorId, string senderName, string senderType,
+        public virtual void OnSendEvent(StateMachineId targetStateMachineId, string senderName, string senderType,
             string senderStateName,
             Event e, Guid opGroupId, bool isTargetHalted)
         {
         }
 
         /// <inheritdoc />
-        public virtual void OnStateTransition(ActorId id, string stateName, bool isEntry)
+        public virtual void OnStateTransition(StateMachineId id, string stateName, bool isEntry)
         {
         }
 
         /// <inheritdoc />
-        public virtual void OnWaitEvent(ActorId id, string stateName, Type eventType)
+        public virtual void OnWaitEvent(StateMachineId id, string stateName, Type eventType)
         {
         }
 
         /// <inheritdoc />
-        public virtual void OnWaitEvent(ActorId id, string stateName, params Type[] eventTypes)
+        public virtual void OnWaitEvent(StateMachineId id, string stateName, params Type[] eventTypes)
         {
         }
 
diff --git a/Src/PChecker/CheckerCore/Actors/Logging/PCheckerLogTextFormatter.cs b/Src/PChecker/CheckerCore/StateMachines/Logging/PCheckerLogTextFormatter.cs
similarity index 82%
rename from Src/PChecker/CheckerCore/Actors/Logging/PCheckerLogTextFormatter.cs
rename to Src/PChecker/CheckerCore/StateMachines/Logging/PCheckerLogTextFormatter.cs
index 17a01458c..b22694712 100644
--- a/Src/PChecker/CheckerCore/Actors/Logging/PCheckerLogTextFormatter.cs
+++ b/Src/PChecker/CheckerCore/StateMachines/Logging/PCheckerLogTextFormatter.cs
@@ -4,15 +4,15 @@
 using System;
 using System.IO;
 using System.Threading.Tasks;
-using PChecker.Actors.Events;
+using PChecker.StateMachines.Events;
 using PChecker.IO.Logging;
 
-namespace PChecker.Actors.Logging
+namespace PChecker.StateMachines.Logging
 {
     /// <summary>
-    /// This class implements IActorRuntimeLog and generates output in a a human readable text format.
+    /// This class implements IStateMachineRuntimeLog and generates output in a a human readable text format.
     /// </summary>
-    public class PCheckerLogTextFormatter : IActorRuntimeLog
+    public class PCheckerLogTextFormatter : IStateMachineRuntimeLog
     {
         /// <summary>
         /// Get or set the TextWriter to write to.
@@ -34,19 +34,7 @@ public virtual void OnAssertionFailure(string error)
         }
 
         /// <inheritdoc/>
-        public virtual void OnCreateActor(ActorId id, string creatorName, string creatorType)
-        {
-            if (id.Name.Contains("GodMachine") || creatorName.Contains("GodMachine"))
-            {
-                return;
-            }
-            var source = creatorName ?? $"task '{Task.CurrentId}'";
-            var text = $"<CreateLog> {id} was created by {source}.";
-            Logger.WriteLine(text);
-        }
-
-        /// <inheritdoc/>
-        public void OnCreateStateMachine(ActorId id, string creatorName, string creatorType)
+        public void OnCreateStateMachine(StateMachineId id, string creatorName, string creatorType)
         {
             if (id.Name.Contains("GodMachine") || creatorName.Contains("GodMachine"))
             {
@@ -65,7 +53,7 @@ public virtual void OnCreateMonitor(string monitorType)
         }
 
         /// <inheritdoc/>
-        public virtual void OnDefaultEventHandler(ActorId id, string stateName)
+        public virtual void OnDefaultEventHandler(StateMachineId id, string stateName)
         {
             string text;
             if (stateName is null)
@@ -81,7 +69,7 @@ public virtual void OnDefaultEventHandler(ActorId id, string stateName)
         }
 
         /// <inheritdoc/>
-        public virtual void OnDequeueEvent(ActorId id, string stateName, Event e)
+        public virtual void OnDequeueEvent(StateMachineId id, string stateName, Event e)
         {
             var eventName = e.GetType().FullName;
             string text;
@@ -98,7 +86,7 @@ public virtual void OnDequeueEvent(ActorId id, string stateName, Event e)
         }
 
         /// <inheritdoc/>
-        public virtual void OnEnqueueEvent(ActorId id, Event e)
+        public virtual void OnEnqueueEvent(StateMachineId id, Event e)
         {
             var eventName = e.GetType().FullName;
             var text = $"<EnqueueLog> {id} enqueued event '{eventName}'.";
@@ -106,7 +94,7 @@ public virtual void OnEnqueueEvent(ActorId id, Event e)
         }
 
         /// <inheritdoc/>
-        public virtual void OnExceptionHandled(ActorId id, string stateName, string actionName, Exception ex)
+        public virtual void OnExceptionHandled(StateMachineId id, string stateName, string actionName, Exception ex)
         {
             string text;
             if (stateName is null)
@@ -122,7 +110,7 @@ public virtual void OnExceptionHandled(ActorId id, string stateName, string acti
         }
 
         /// <inheritdoc/>
-        public virtual void OnExceptionThrown(ActorId id, string stateName, string actionName, Exception ex)
+        public virtual void OnExceptionThrown(StateMachineId id, string stateName, string actionName, Exception ex)
         {
             string text;
             if (stateName is null)
@@ -138,7 +126,7 @@ public virtual void OnExceptionThrown(ActorId id, string stateName, string actio
         }
 
         /// <inheritdoc/>
-        public virtual void OnExecuteAction(ActorId id, string handlingStateName, string currentStateName, string actionName)
+        public virtual void OnExecuteAction(StateMachineId id, string handlingStateName, string currentStateName, string actionName)
         {
             string text;
             if (currentStateName is null)
@@ -158,21 +146,21 @@ public virtual void OnExecuteAction(ActorId id, string handlingStateName, string
         }
 
         /// <inheritdoc/>
-        public virtual void OnGotoState(ActorId id, string currentStateName, string newStateName)
+        public virtual void OnGotoState(StateMachineId id, string currentStateName, string newStateName)
         {
             var text = $"<GotoLog> {id} is transitioning from state '{currentStateName}' to state '{newStateName}'.";
             Logger.WriteLine(text);
         }
 
         /// <inheritdoc/>
-        public virtual void OnHalt(ActorId id, int inboxSize)
+        public virtual void OnHalt(StateMachineId id, int inboxSize)
         {
             var text = $"<HaltLog> {id} halted with {inboxSize} events in its inbox.";
             Logger.WriteLine(text);
         }
 
         /// <inheritdoc/>
-        public virtual void OnHandleRaisedEvent(ActorId id, string stateName, Event e)
+        public virtual void OnHandleRaisedEvent(StateMachineId id, string stateName, Event e)
         {
         }
 
@@ -214,7 +202,7 @@ public virtual void OnMonitorError(string monitorType, string stateName, bool? i
         }
 
         /// <inheritdoc/>
-        public virtual void OnPopState(ActorId id, string currentStateName, string restoredStateName)
+        public virtual void OnPopState(StateMachineId id, string currentStateName, string restoredStateName)
         {
             currentStateName = string.IsNullOrEmpty(currentStateName) ? "[not recorded]" : currentStateName;
             var reenteredStateName = restoredStateName ?? string.Empty;
@@ -223,7 +211,7 @@ public virtual void OnPopState(ActorId id, string currentStateName, string resto
         }
 
         /// <inheritdoc/>
-        public virtual void OnPopStateUnhandledEvent(ActorId id, string stateName, Event e)
+        public virtual void OnPopStateUnhandledEvent(StateMachineId id, string stateName, Event e)
         {
             var eventName = e.GetType().Name;
             var text = $"<PopLog> {id} popped state {stateName} due to unhandled event '{eventName}'.";
@@ -231,14 +219,14 @@ public virtual void OnPopStateUnhandledEvent(ActorId id, string stateName, Event
         }
 
         /// <inheritdoc/>
-        public virtual void OnPushState(ActorId id, string currentStateName, string newStateName)
+        public virtual void OnPushState(StateMachineId id, string currentStateName, string newStateName)
         {
             var text = $"<PushLog> {id} pushed from state '{currentStateName}' to state '{newStateName}'.";
             Logger.WriteLine(text);
         }
 
         /// <inheritdoc/>
-        public virtual void OnRaiseEvent(ActorId id, string stateName, Event e)
+        public virtual void OnRaiseEvent(StateMachineId id, string stateName, Event e)
         {
             var eventName = e.GetType().FullName;
             string text;
@@ -255,7 +243,7 @@ public virtual void OnRaiseEvent(ActorId id, string stateName, Event e)
         }
 
         /// <inheritdoc/>
-        public virtual void OnReceiveEvent(ActorId id, string stateName, Event e, bool wasBlocked)
+        public virtual void OnReceiveEvent(StateMachineId id, string stateName, Event e, bool wasBlocked)
         {
             var eventName = e.GetType().FullName;
             string text;
@@ -273,19 +261,19 @@ public virtual void OnReceiveEvent(ActorId id, string stateName, Event e, bool w
         }
 
         /// <inheritdoc/>
-        public virtual void OnSendEvent(ActorId targetActorId, string senderName, string senderType, string senderStateName,
+        public virtual void OnSendEvent(StateMachineId targetStateMachineId, string senderName, string senderType, string senderStateName,
             Event e, Guid opGroupId, bool isTargetHalted)
         {
             var opGroupIdMsg = opGroupId != Guid.Empty ? $" (operation group '{opGroupId}')" : string.Empty;
             var isHalted = isTargetHalted ? $" which has halted" : string.Empty;
             var sender = senderName != null ? $"{senderName} in state '{senderStateName}'" : $"task '{Task.CurrentId}'";
             var eventName = e.GetType().FullName;
-            var text = $"<SendLog> {sender} sent event '{eventName}' to {targetActorId}{isHalted}{opGroupIdMsg}.";
+            var text = $"<SendLog> {sender} sent event '{eventName}' to {targetStateMachineId}{isHalted}{opGroupIdMsg}.";
             Logger.WriteLine(text);
         }
 
         /// <inheritdoc/>
-        public virtual void OnStateTransition(ActorId id, string stateName, bool isEntry)
+        public virtual void OnStateTransition(StateMachineId id, string stateName, bool isEntry)
         {
             var direction = isEntry ? "enters" : "exits";
             var text = $"<StateLog> {id} {direction} state '{stateName}'.";
@@ -301,7 +289,7 @@ public virtual void OnStrategyDescription(string strategyName, string descriptio
         }
 
         /// <inheritdoc/>
-        public virtual void OnWaitEvent(ActorId id, string stateName, Type eventType)
+        public virtual void OnWaitEvent(StateMachineId id, string stateName, Type eventType)
         {
             string text;
             if (stateName is null)
@@ -317,7 +305,7 @@ public virtual void OnWaitEvent(ActorId id, string stateName, Type eventType)
         }
 
         /// <inheritdoc/>
-        public virtual void OnWaitEvent(ActorId id, string stateName, params Type[] eventTypes)
+        public virtual void OnWaitEvent(StateMachineId id, string stateName, params Type[] eventTypes)
         {
             string text;
             string eventNames;
diff --git a/Src/PChecker/CheckerCore/Actors/Logging/PCheckerLogXmlFormatter.cs b/Src/PChecker/CheckerCore/StateMachines/Logging/PCheckerLogXmlFormatter.cs
similarity index 84%
rename from Src/PChecker/CheckerCore/Actors/Logging/PCheckerLogXmlFormatter.cs
rename to Src/PChecker/CheckerCore/StateMachines/Logging/PCheckerLogXmlFormatter.cs
index 87954b2ae..148fc364c 100644
--- a/Src/PChecker/CheckerCore/Actors/Logging/PCheckerLogXmlFormatter.cs
+++ b/Src/PChecker/CheckerCore/StateMachines/Logging/PCheckerLogXmlFormatter.cs
@@ -5,14 +5,14 @@
 using System.Text;
 using System.Threading.Tasks;
 using System.Xml;
-using PChecker.Actors.Events;
+using PChecker.StateMachines.Events;
 
-namespace PChecker.Actors.Logging
+namespace PChecker.StateMachines.Logging
 {
     /// <summary>
-    /// This class implements IActorRuntimeLog and generates log output in an XML format.
+    /// This class implements IStateMachineRuntimeLog and generates log output in an XML format.
     /// </summary>
-    internal class PCheckerLogXmlFormatter : IActorRuntimeLog
+    internal class PCheckerLogXmlFormatter : IStateMachineRuntimeLog
     {
         private readonly XmlWriter Writer;
         private bool Closed;
@@ -44,33 +44,9 @@ public void OnAssertionFailure(string error)
 
             Writer.WriteElementString("AssertionFailure", error);
         }
-
-        public void OnCreateActor(ActorId id, string creatorName, string creatorType)
-        {
-            if (Closed)
-            {
-                return;
-            }
-
-            Writer.WriteStartElement("CreateActor");
-            Writer.WriteAttributeString("id", id.ToString());
-
-            if (creatorName != null && creatorType != null)
-            {
-                Writer.WriteAttributeString("creatorName", creatorName);
-                Writer.WriteAttributeString("creatorType", creatorType);
-            }
-            else
-            {
-                Writer.WriteAttributeString("creatorName", Task.CurrentId.ToString());
-                Writer.WriteAttributeString("creatorType", "task");
-            }
-
-            Writer.WriteEndElement();
-        }
-
+        
         /// <inheritdoc/>
-        public void OnCreateStateMachine(ActorId id, string creatorName, string creatorType)
+        public void OnCreateStateMachine(StateMachineId id, string creatorName, string creatorType)
         {
             if (Closed)
             {
@@ -94,7 +70,7 @@ public void OnCreateStateMachine(ActorId id, string creatorName, string creatorT
             Writer.WriteEndElement();
         }
 
-        public void OnDefaultEventHandler(ActorId id, string stateName)
+        public void OnDefaultEventHandler(StateMachineId id, string stateName)
         {
             if (Closed)
             {
@@ -111,7 +87,7 @@ public void OnDefaultEventHandler(ActorId id, string stateName)
             Writer.WriteEndElement();
         }
 
-        public void OnDequeueEvent(ActorId id, string stateName, Event e)
+        public void OnDequeueEvent(StateMachineId id, string stateName, Event e)
         {
             if (Closed)
             {
@@ -129,7 +105,7 @@ public void OnDequeueEvent(ActorId id, string stateName, Event e)
             Writer.WriteEndElement();
         }
 
-        public void OnEnqueueEvent(ActorId id, Event e)
+        public void OnEnqueueEvent(StateMachineId id, Event e)
         {
             if (Closed)
             {
@@ -142,7 +118,7 @@ public void OnEnqueueEvent(ActorId id, Event e)
             Writer.WriteEndElement();
         }
 
-        public void OnExceptionHandled(ActorId id, string stateName, string actionName, Exception ex)
+        public void OnExceptionHandled(StateMachineId id, string stateName, string actionName, Exception ex)
         {
             if (Closed)
             {
@@ -162,7 +138,7 @@ public void OnExceptionHandled(ActorId id, string stateName, string actionName,
             Writer.WriteEndElement();
         }
 
-        public void OnExceptionThrown(ActorId id, string stateName, string actionName, Exception ex)
+        public void OnExceptionThrown(StateMachineId id, string stateName, string actionName, Exception ex)
         {
             if (Closed)
             {
@@ -178,7 +154,7 @@ public void OnExceptionThrown(ActorId id, string stateName, string actionName, E
             Writer.WriteEndElement();
         }
 
-        public void OnExecuteAction(ActorId id, string handlingStateName, string currentStateName, string actionName)
+        public void OnExecuteAction(StateMachineId id, string handlingStateName, string currentStateName, string actionName)
         {
             if (Closed)
             {
@@ -200,7 +176,7 @@ public void OnExecuteAction(ActorId id, string handlingStateName, string current
             Writer.WriteEndElement();
         }
 
-        public void OnGotoState(ActorId id, string currentStateName, string newStateName)
+        public void OnGotoState(StateMachineId id, string currentStateName, string newStateName)
         {
             if (Closed)
             {
@@ -214,7 +190,7 @@ public void OnGotoState(ActorId id, string currentStateName, string newStateName
             Writer.WriteEndElement();
         }
 
-        public void OnHalt(ActorId id, int inboxSize)
+        public void OnHalt(StateMachineId id, int inboxSize)
         {
             if (Closed)
             {
@@ -227,7 +203,7 @@ public void OnHalt(ActorId id, int inboxSize)
             Writer.WriteEndElement();
         }
 
-        public void OnHandleRaisedEvent(ActorId id, string stateName, Event e)
+        public void OnHandleRaisedEvent(StateMachineId id, string stateName, Event e)
         {
             if (Closed)
             {
@@ -235,7 +211,7 @@ public void OnHandleRaisedEvent(ActorId id, string stateName, Event e)
             }
         }
 
-        public void OnPopState(ActorId id, string currentStateName, string restoredStateName)
+        public void OnPopState(StateMachineId id, string currentStateName, string restoredStateName)
         {
             if (Closed)
             {
@@ -249,7 +225,7 @@ public void OnPopState(ActorId id, string currentStateName, string restoredState
             Writer.WriteEndElement();
         }
 
-        public void OnPopStateUnhandledEvent(ActorId id, string stateName, Event e)
+        public void OnPopStateUnhandledEvent(StateMachineId id, string stateName, Event e)
         {
             if (Closed)
             {
@@ -263,7 +239,7 @@ public void OnPopStateUnhandledEvent(ActorId id, string stateName, Event e)
             Writer.WriteEndElement();
         }
 
-        public void OnPushState(ActorId id, string currentStateName, string newStateName)
+        public void OnPushState(StateMachineId id, string currentStateName, string newStateName)
         {
             if (Closed)
             {
@@ -277,7 +253,7 @@ public void OnPushState(ActorId id, string currentStateName, string newStateName
             Writer.WriteEndElement();
         }
 
-        public void OnRaiseEvent(ActorId id, string stateName, Event e)
+        public void OnRaiseEvent(StateMachineId id, string stateName, Event e)
         {
             if (Closed)
             {
@@ -295,7 +271,7 @@ public void OnRaiseEvent(ActorId id, string stateName, Event e)
             Writer.WriteEndElement();
         }
 
-        public void OnReceiveEvent(ActorId id, string stateName, Event e, bool wasBlocked)
+        public void OnReceiveEvent(StateMachineId id, string stateName, Event e, bool wasBlocked)
         {
             if (Closed)
             {
@@ -315,7 +291,7 @@ public void OnReceiveEvent(ActorId id, string stateName, Event e, bool wasBlocke
             Writer.WriteEndElement();
         }
 
-        public void OnSendEvent(ActorId targetActorId, string senderName, string senderType, string senderStateName,
+        public void OnSendEvent(StateMachineId targetStateMachineId, string senderName, string senderType, string senderStateName,
             Event e, Guid opGroupId, bool isTargetHalted)
         {
             if (Closed)
@@ -324,7 +300,7 @@ public void OnSendEvent(ActorId targetActorId, string senderName, string senderT
             }
 
             Writer.WriteStartElement("Send");
-            Writer.WriteAttributeString("target", targetActorId.ToString());
+            Writer.WriteAttributeString("target", targetStateMachineId.ToString());
 
             if (senderName != null && senderType != null)
             {
@@ -345,7 +321,7 @@ public void OnSendEvent(ActorId targetActorId, string senderName, string senderT
             Writer.WriteEndElement();
         }
 
-        public void OnStateTransition(ActorId id, string stateName, bool isEntry)
+        public void OnStateTransition(StateMachineId id, string stateName, bool isEntry)
         {
             if (Closed)
             {
@@ -359,7 +335,7 @@ public void OnStateTransition(ActorId id, string stateName, bool isEntry)
             Writer.WriteEndElement();
         }
 
-        public void OnWaitEvent(ActorId id, string stateName, Type eventType)
+        public void OnWaitEvent(StateMachineId id, string stateName, Type eventType)
         {
             if (Closed)
             {
@@ -377,7 +353,7 @@ public void OnWaitEvent(ActorId id, string stateName, Type eventType)
             Writer.WriteEndElement();
         }
 
-        public void OnWaitEvent(ActorId id, string stateName, params Type[] eventTypes)
+        public void OnWaitEvent(StateMachineId id, string stateName, params Type[] eventTypes)
         {
             if (Closed)
             {
diff --git a/Src/PChecker/CheckerCore/Actors/Managers/IStateMachineManager.cs b/Src/PChecker/CheckerCore/StateMachines/Managers/IStateMachineManager.cs
similarity index 97%
rename from Src/PChecker/CheckerCore/Actors/Managers/IStateMachineManager.cs
rename to Src/PChecker/CheckerCore/StateMachines/Managers/IStateMachineManager.cs
index 35045bda4..a87b75bfd 100644
--- a/Src/PChecker/CheckerCore/Actors/Managers/IStateMachineManager.cs
+++ b/Src/PChecker/CheckerCore/StateMachines/Managers/IStateMachineManager.cs
@@ -3,9 +3,9 @@
 
 using System;
 using System.Collections.Generic;
-using PChecker.Actors.Events;
+using PChecker.StateMachines.Events;
 
-namespace PChecker.Actors.Managers
+namespace PChecker.StateMachines.Managers
 {
     /// <summary>
     /// Interface for managing a state machine.
diff --git a/Src/PChecker/CheckerCore/Actors/Managers/StateMachineManager.cs b/Src/PChecker/CheckerCore/StateMachines/Managers/StateMachineManager.cs
similarity index 98%
rename from Src/PChecker/CheckerCore/Actors/Managers/StateMachineManager.cs
rename to Src/PChecker/CheckerCore/StateMachines/Managers/StateMachineManager.cs
index c1a9b1f12..f648fd050 100644
--- a/Src/PChecker/CheckerCore/Actors/Managers/StateMachineManager.cs
+++ b/Src/PChecker/CheckerCore/StateMachines/Managers/StateMachineManager.cs
@@ -4,10 +4,10 @@
 using System;
 using System.Collections.Generic;
 using System.Runtime.CompilerServices;
-using PChecker.Actors.Events;
+using PChecker.StateMachines.Events;
 using PChecker.SystematicTesting;
 
-namespace PChecker.Actors.Managers.Mocks
+namespace PChecker.StateMachines.Managers.Mocks
 {
     /// <summary>
     /// Implements a state machine manager that is used during testing.
diff --git a/Src/PChecker/CheckerCore/Actors/NameResolver.cs b/Src/PChecker/CheckerCore/StateMachines/NameResolver.cs
similarity index 98%
rename from Src/PChecker/CheckerCore/Actors/NameResolver.cs
rename to Src/PChecker/CheckerCore/StateMachines/NameResolver.cs
index 17cee7344..3a32fe554 100644
--- a/Src/PChecker/CheckerCore/Actors/NameResolver.cs
+++ b/Src/PChecker/CheckerCore/StateMachines/NameResolver.cs
@@ -5,7 +5,7 @@
 using System.Collections.Concurrent;
 using System.Globalization;
 
-namespace PChecker.Actors
+namespace PChecker.StateMachines
 {
     /// <summary>
     /// Utility class for resolving names.
diff --git a/Src/PChecker/CheckerCore/Actors/StateMachine.cs b/Src/PChecker/CheckerCore/StateMachines/StateMachine.cs
similarity index 98%
rename from Src/PChecker/CheckerCore/Actors/StateMachine.cs
rename to Src/PChecker/CheckerCore/StateMachines/StateMachine.cs
index 2c2affef3..241a112a1 100644
--- a/Src/PChecker/CheckerCore/Actors/StateMachine.cs
+++ b/Src/PChecker/CheckerCore/StateMachines/StateMachine.cs
@@ -11,20 +11,20 @@
 using System.Reflection;
 using System.Runtime.CompilerServices;
 using System.Threading.Tasks;
-using PChecker.Actors.EventQueues;
-using PChecker.Actors.Events;
-using PChecker.Actors.Exceptions;
-using PChecker.Actors.Handlers;
-using PChecker.Actors.Logging;
-using PChecker.Actors.Managers;
-using PChecker.Actors.StateTransitions;
+using PChecker.StateMachines.EventQueues;
+using PChecker.StateMachines.Events;
+using PChecker.StateMachines.Exceptions;
+using PChecker.StateMachines.Handlers;
+using PChecker.StateMachines.Logging;
+using PChecker.StateMachines.Managers;
+using PChecker.StateMachines.StateTransitions;
 using PChecker.Exceptions;
 using PChecker.IO.Debugging;
 using PChecker.SystematicTesting;
-using EventInfo = PChecker.Actors.Events.EventInfo;
+using EventInfo = PChecker.StateMachines.Events.EventInfo;
 
 
-namespace PChecker.Actors
+namespace PChecker.StateMachines
 {
     /// <summary>
     /// Type that implements a state machine with states, state transitions and event handlers.
@@ -40,7 +40,7 @@ public abstract class StateMachine
         /// <summary>
         /// Unique id that identifies this state machine.
         /// </summary>
-        protected internal ActorId Id { get; private set; }
+        protected internal StateMachineId Id { get; private set; }
 
         /// <summary>
         /// Manages the state machine.
@@ -156,7 +156,7 @@ protected StateMachine()
         /// <summary>
         /// Configures the state machine.
         /// </summary>
-        internal void Configure(ControlledRuntime runtime, ActorId id, IStateMachineManager manager, IEventQueue inbox)
+        internal void Configure(ControlledRuntime runtime, StateMachineId id, IStateMachineManager manager, IEventQueue inbox)
         {
             Runtime = runtime;
             Id = id;
@@ -396,8 +396,8 @@ protected internal Guid OperationGroupId
         /// <param name="initialEvent">Optional initialization event.</param>
         /// <param name="opGroupId">Optional id that can be used to identify this operation.</param>
         /// <returns>The unique state machine id.</returns>
-        protected ActorId CreateActor(Type type, string name, Event initialEvent = null, Guid opGroupId = default) =>
-            Runtime.CreateActor(null, type, name, initialEvent, this, opGroupId);
+        protected StateMachineId CreateStateMachine(Type type, string name, Event initialEvent = null, Guid opGroupId = default) =>
+            Runtime.CreateStateMachine(null, type, name, initialEvent, this, opGroupId);
         
         
         /// <summary>
@@ -406,7 +406,7 @@ protected ActorId CreateActor(Type type, string name, Event initialEvent = null,
         /// <param name="id">The id of the target.</param>
         /// <param name="e">The event to send.</param>
         /// <param name="opGroupId">Optional id that can be used to identify this operation.</param>
-        protected void SendEvent(ActorId id, Event e, Guid opGroupId = default) =>
+        protected void SendEvent(StateMachineId id, Event e, Guid opGroupId = default) =>
             Runtime.SendEvent(id, e, this, opGroupId);
         
         /// <summary>
@@ -611,21 +611,21 @@ private protected async Task InvokeActionAsync(CachedDelegate cachedAction, Even
         private protected MethodInfo GetActionWithName(string actionName)
         {
             MethodInfo action;
-            var actorType = GetType();
+            var stateMachineType = GetType();
 
             do
             {
                 var bindingFlags = BindingFlags.Public | BindingFlags.NonPublic |
                                    BindingFlags.Instance | BindingFlags.FlattenHierarchy;
-                action = actorType.GetMethod(actionName, bindingFlags, Type.DefaultBinder, SingleEventTypeArray, null);
+                action = stateMachineType.GetMethod(actionName, bindingFlags, Type.DefaultBinder, SingleEventTypeArray, null);
                 if (action is null)
                 {
-                    action = actorType.GetMethod(actionName, bindingFlags, Type.DefaultBinder, Array.Empty<Type>(), null);
+                    action = stateMachineType.GetMethod(actionName, bindingFlags, Type.DefaultBinder, Array.Empty<Type>(), null);
                 }
 
-                actorType = actorType.BaseType;
+                stateMachineType = stateMachineType.BaseType;
             }
-            while (action is null && actorType != typeof(StateMachine));
+            while (action is null && stateMachineType != typeof(StateMachine));
 
             Assert(action != null, "Cannot detect action declaration '{0}' in '{1}'.", actionName, GetType().FullName);
             AssertActionValidity(action);
diff --git a/Src/PChecker/CheckerCore/Actors/StateMachineFactory.cs b/Src/PChecker/CheckerCore/StateMachines/StateMachineFactory.cs
similarity index 98%
rename from Src/PChecker/CheckerCore/Actors/StateMachineFactory.cs
rename to Src/PChecker/CheckerCore/StateMachines/StateMachineFactory.cs
index 7ce615311..f3c2b84e9 100644
--- a/Src/PChecker/CheckerCore/Actors/StateMachineFactory.cs
+++ b/Src/PChecker/CheckerCore/StateMachines/StateMachineFactory.cs
@@ -5,7 +5,7 @@
 using System.Collections.Generic;
 using System.Linq.Expressions;
 
-namespace PChecker.Actors
+namespace PChecker.StateMachines
 {
     /// <summary>
     /// Factory for creating state machine instances.
diff --git a/Src/PChecker/CheckerCore/Actors/ActorId.cs b/Src/PChecker/CheckerCore/StateMachines/StateMachineId.cs
similarity index 69%
rename from Src/PChecker/CheckerCore/Actors/ActorId.cs
rename to Src/PChecker/CheckerCore/StateMachines/StateMachineId.cs
index 3c08aa10b..113481c54 100644
--- a/Src/PChecker/CheckerCore/Actors/ActorId.cs
+++ b/Src/PChecker/CheckerCore/StateMachines/StateMachineId.cs
@@ -4,20 +4,21 @@
 using System;
 using System.Globalization;
 using System.Runtime.Serialization;
+using PChecker.StateMachines;
 using PChecker.SystematicTesting;
 
-namespace PChecker.Actors
+namespace PChecker.StateMachines
 {
     /// <summary>
-    /// Unique actor id.
+    /// Unique state machine id.
     /// </summary>
     [DataContract]
-    public sealed class ActorId : IEquatable<ActorId>, IComparable<ActorId>
+    public sealed class StateMachineId : IEquatable<StateMachineId>, IComparable<StateMachineId>
     {
         /// <summary>
-        /// The runtime that executes the actor with this id.
+        /// The runtime that executes the state machine with this id.
         /// </summary>
-        public IActorRuntime Runtime { get; private set; }
+        public IStateMachineRuntime Runtime { get; private set; }
 
         /// <summary>
         /// Unique id, when <see cref="NameValue"/> is empty.
@@ -32,7 +33,7 @@ public sealed class ActorId : IEquatable<ActorId>, IComparable<ActorId>
         public readonly string NameValue;
 
         /// <summary>
-        /// The type of the actor associated with this id.
+        /// The type of the state machine associated with this id.
         /// </summary>
         [DataMember]
         public readonly string Type;
@@ -44,7 +45,7 @@ public sealed class ActorId : IEquatable<ActorId>, IComparable<ActorId>
         public readonly string Name;
 
         /// <summary>
-        /// Generation of the runtime that created this actor id.
+        /// Generation of the runtime that created this state machine id.
         /// </summary>
         [DataMember]
         public readonly ulong Generation;
@@ -61,9 +62,9 @@ public sealed class ActorId : IEquatable<ActorId>, IComparable<ActorId>
         public bool IsNameUsedForHashing => NameValue.Length > 0;
 
         /// <summary>
-        /// Initializes a new instance of the <see cref="ActorId"/> class.
+        /// Initializes a new instance of the <see cref="StateMachineId"/> class.
         /// </summary>
-        internal ActorId(Type type, string name, ControlledRuntime runtime, bool useNameForHashing = false)
+        internal StateMachineId(Type type, string name, ControlledRuntime runtime, bool useNameForHashing = false)
         {
             Runtime = runtime;
             Endpoint = string.Empty;
@@ -72,7 +73,7 @@ internal ActorId(Type type, string name, ControlledRuntime runtime, bool useName
             {
                 Value = 0;
                 NameValue = name;
-                Runtime.Assert(!string.IsNullOrEmpty(NameValue), "The actor name cannot be null when used as id.");
+                Runtime.Assert(!string.IsNullOrEmpty(NameValue), "The state machine name cannot be null when used as id.");
             }
             else
             {
@@ -80,7 +81,7 @@ internal ActorId(Type type, string name, ControlledRuntime runtime, bool useName
                 NameValue = string.Empty;
 
                 // Checks for overflow.
-                Runtime.Assert(Value != ulong.MaxValue, "Detected actor id overflow.");
+                Runtime.Assert(Value != ulong.MaxValue, "Detected state machine id overflow.");
             }
 
             Type = type.FullName;
@@ -96,7 +97,7 @@ internal ActorId(Type type, string name, ControlledRuntime runtime, bool useName
         }
 
         /// <summary>
-        /// Bind the actor id.
+        /// Bind the state machine id.
         /// </summary>
         internal void Bind(ControlledRuntime runtime)
         {
@@ -108,7 +109,7 @@ internal void Bind(ControlledRuntime runtime)
         /// </summary>
         public override bool Equals(object obj)
         {
-            if (obj is ActorId id)
+            if (obj is StateMachineId id)
             {
                 // Use same machanism for hashing.
                 if (IsNameUsedForHashing != id.IsNameUsedForHashing)
@@ -136,24 +137,24 @@ public override int GetHashCode()
         }
 
         /// <summary>
-        /// Returns a string that represents the current actor id.
+        /// Returns a string that represents the current state machine id.
         /// </summary>
         public override string ToString() => Name;
 
         /// <summary>
-        /// Indicates whether the specified <see cref="ActorId"/> is equal
-        /// to the current <see cref="ActorId"/>.
+        /// Indicates whether the specified <see cref="StateMachineId"/> is equal
+        /// to the current <see cref="StateMachineId"/>.
         /// </summary>
-        public bool Equals(ActorId other) => Equals((object)other);
+        public bool Equals(StateMachineId other) => Equals((object)other);
 
         /// <summary>
-        /// Compares the specified <see cref="ActorId"/> with the current
-        /// <see cref="ActorId"/> for ordering or sorting purposes.
+        /// Compares the specified <see cref="StateMachineId"/> with the current
+        /// <see cref="StateMachineId"/> for ordering or sorting purposes.
         /// </summary>
-        public int CompareTo(ActorId other) => string.Compare(Name, other?.Name);
+        public int CompareTo(StateMachineId other) => string.Compare(Name, other?.Name);
 
-        bool IEquatable<ActorId>.Equals(ActorId other) => Equals(other);
+        bool IEquatable<StateMachineId>.Equals(StateMachineId other) => Equals(other);
 
-        int IComparable<ActorId>.CompareTo(ActorId other) => string.Compare(Name, other?.Name);
+        int IComparable<StateMachineId>.CompareTo(StateMachineId other) => string.Compare(Name, other?.Name);
     }
 }
\ No newline at end of file
diff --git a/Src/PChecker/CheckerCore/Actors/StateTransitions/GotoStateTransition.cs b/Src/PChecker/CheckerCore/StateMachines/StateTransitions/GotoStateTransition.cs
similarity index 94%
rename from Src/PChecker/CheckerCore/Actors/StateTransitions/GotoStateTransition.cs
rename to Src/PChecker/CheckerCore/StateMachines/StateTransitions/GotoStateTransition.cs
index 2b41829ac..bc69d2728 100644
--- a/Src/PChecker/CheckerCore/Actors/StateTransitions/GotoStateTransition.cs
+++ b/Src/PChecker/CheckerCore/StateMachines/StateTransitions/GotoStateTransition.cs
@@ -2,9 +2,9 @@
 // Licensed under the MIT License.
 
 using System;
-using PChecker.Actors.Handlers;
+using PChecker.StateMachines.Handlers;
 
-namespace PChecker.Actors.StateTransitions
+namespace PChecker.StateMachines.StateTransitions
 {
     /// <summary>
     /// Defines a goto state transition.
diff --git a/Src/PChecker/CheckerCore/Actors/StateTransitions/PushStateTransition.cs b/Src/PChecker/CheckerCore/StateMachines/StateTransitions/PushStateTransition.cs
similarity index 89%
rename from Src/PChecker/CheckerCore/Actors/StateTransitions/PushStateTransition.cs
rename to Src/PChecker/CheckerCore/StateMachines/StateTransitions/PushStateTransition.cs
index da0f64c51..b721319d5 100644
--- a/Src/PChecker/CheckerCore/Actors/StateTransitions/PushStateTransition.cs
+++ b/Src/PChecker/CheckerCore/StateMachines/StateTransitions/PushStateTransition.cs
@@ -2,9 +2,9 @@
 // Licensed under the MIT License.
 
 using System;
-using PChecker.Actors.Handlers;
+using PChecker.StateMachines.Handlers;
 
-namespace PChecker.Actors.StateTransitions
+namespace PChecker.StateMachines.StateTransitions
 {
     /// <summary>
     /// Defines a push state transition.
diff --git a/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs b/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs
index c9b3911bf..69c75d0cd 100644
--- a/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs
+++ b/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs
@@ -11,14 +11,14 @@
 using System.Linq.Expressions;
 using System.Reflection;
 using System.Threading.Tasks;
-using PChecker.Actors;
-using PChecker.Actors.EventQueues;
-using PChecker.Actors.EventQueues.Mocks;
-using PChecker.Actors.Events;
-using PChecker.Actors.Exceptions;
-using PChecker.Actors.Logging;
-using PChecker.Actors.Managers;
-using PChecker.Actors.Managers.Mocks;
+using PChecker.StateMachines;
+using PChecker.StateMachines.EventQueues;
+using PChecker.StateMachines.EventQueues.Mocks;
+using PChecker.StateMachines.Events;
+using PChecker.StateMachines.Exceptions;
+using PChecker.StateMachines.Logging;
+using PChecker.StateMachines.Managers;
+using PChecker.StateMachines.Managers.Mocks;
 using PChecker.Coverage;
 using PChecker.Exceptions;
 using PChecker.Random;
@@ -29,14 +29,14 @@
 using PChecker.SystematicTesting.Strategies.Liveness;
 using PChecker.SystematicTesting.Traces;
 using Debug = PChecker.IO.Debugging.Debug;
-using EventInfo = PChecker.Actors.Events.EventInfo;
+using EventInfo = PChecker.StateMachines.Events.EventInfo;
 
 namespace PChecker.SystematicTesting
 {
     /// <summary>
     /// Runtime for controlling asynchronous operations.
     /// </summary>
-    internal sealed class ControlledRuntime : CoyoteRuntime, IActorRuntime
+    internal sealed class ControlledRuntime : CoyoteRuntime, IStateMachineRuntime
     {
         
         /// <summary>
@@ -60,9 +60,9 @@ internal sealed class ControlledRuntime : CoyoteRuntime, IActorRuntime
         internal CoverageInfo CoverageInfo;
 
         /// <summary>
-        /// Map that stores all unique names and their corresponding actor ids.
+        /// Map that stores all unique names and their corresponding state machine ids.
         /// </summary>
-        internal readonly ConcurrentDictionary<string, ActorId> NameValueToActorId;
+        internal readonly ConcurrentDictionary<string, StateMachineId> NameValueToStateMachineId;
 
         /// <summary>
         /// The root task id.
@@ -76,9 +76,9 @@ internal sealed class ControlledRuntime : CoyoteRuntime, IActorRuntime
             new Dictionary<Type, Func<StateMachine>>();
         
         /// <summary>
-        /// Map from unique actor ids to state machines.
+        /// Map from unique state machine ids to state machines.
         /// </summary>
-        private readonly ConcurrentDictionary<ActorId, StateMachine> StateMachineMap;
+        private readonly ConcurrentDictionary<StateMachineId, StateMachine> StateMachineMap;
         
         /// <summary>
         /// Callback that is fired when a Coyote event is dropped.
@@ -86,7 +86,7 @@ internal sealed class ControlledRuntime : CoyoteRuntime, IActorRuntime
         public event OnEventDroppedHandler OnEventDropped;
         
         /// <summary>
-        /// Responsible for writing to all registered <see cref="IActorRuntimeLog"/> objects.
+        /// Responsible for writing to all registered <see cref="IStateMachineRuntimeLog"/> objects.
         /// </summary>
         protected internal LogWriter LogWriter { get; private set; }
 
@@ -141,10 +141,10 @@ internal int GetHashedProgramState()
 
                 foreach (var operation in Scheduler.GetRegisteredOperations().OrderBy(op => op.Id))
                 {
-                    if (operation is ActorOperation actorOperation)
+                    if (operation is StateMachineOperation stateMachineOperation)
                     {
-                        int operationHash = 31 + actorOperation.Actor.GetHashedState();
-                        operationHash = (operationHash * 31) + actorOperation.Type.GetHashCode();
+                        int operationHash = 31 + stateMachineOperation.StateMachine.GetHashedState();
+                        operationHash = (operationHash * 31) + stateMachineOperation.Type.GetHashCode();
                         hash *= operationHash;
                     }
                     else if (operation is TaskOperation taskOperation)
@@ -165,13 +165,13 @@ internal ControlledRuntime(CheckerConfiguration checkerConfiguration, ISchedulin
             IRandomValueGenerator valueGenerator)
             : base(checkerConfiguration, valueGenerator)
         {
-            StateMachineMap = new ConcurrentDictionary<ActorId, StateMachine>();
+            StateMachineMap = new ConcurrentDictionary<StateMachineId, StateMachine>();
             LogWriter = new LogWriter(checkerConfiguration);
             
             IsExecutionControlled = true;
 
             RootTaskId = Task.CurrentId;
-            NameValueToActorId = new ConcurrentDictionary<string, ActorId>();
+            NameValueToStateMachineId = new ConcurrentDictionary<string, StateMachineId>();
 
             CoverageInfo = new CoverageInfo();
 
@@ -196,13 +196,13 @@ internal ControlledRuntime(CheckerConfiguration checkerConfiguration,
             IRandomValueGenerator valueGenerator)
             : base(checkerConfiguration, valueGenerator)
         {
-            StateMachineMap = new ConcurrentDictionary<ActorId, StateMachine>();
+            StateMachineMap = new ConcurrentDictionary<StateMachineId, StateMachine>();
             LogWriter = new LogWriter(checkerConfiguration);
             
             IsExecutionControlled = true;
 
             RootTaskId = Task.CurrentId;
-            NameValueToActorId = new ConcurrentDictionary<string, ActorId>();
+            NameValueToStateMachineId = new ConcurrentDictionary<string, StateMachineId>();
 
             CoverageInfo = new CoverageInfo();
             
@@ -214,20 +214,20 @@ internal ControlledRuntime(CheckerConfiguration checkerConfiguration,
         /// <summary>
         /// Creates a fresh state machine id that has not yet been bound to any state machine.
         /// </summary>
-        public ActorId CreateActorId(Type type, string name = null) => new ActorId(type, name, this);
+        public StateMachineId CreateStateMachineId(Type type, string name = null) => new StateMachineId(type, name, this);
 
         /// <summary>
-        /// Creates an actor id that is uniquely tied to the specified unique name. The
-        /// returned actor id can either be a fresh id (not yet bound to any state machine), or
-        /// it can be bound to a previously created state machine. In the second case, this actor
-        /// id can be directly used to communicate with the corresponding actor.
+        /// Creates an state machine id that is uniquely tied to the specified unique name. The
+        /// returned state machine id can either be a fresh id (not yet bound to any state machine), or
+        /// it can be bound to a previously created state machine. In the second case, this state machine
+        /// id can be directly used to communicate with the corresponding state machine.
         /// </summary>
-        public ActorId CreateActorIdFromName(Type type, string name)
+        public StateMachineId CreateStateMachineIdFromName(Type type, string name)
         {
-            // It is important that all actor ids use the monotonically incrementing
+            // It is important that all state machine ids use the monotonically incrementing
             // value as the id during testing, and not the unique name.
-            var id = new ActorId(type, name, this);
-            return NameValueToActorId.GetOrAdd(name, id);
+            var id = new StateMachineId(type, name, this);
+            return NameValueToStateMachineId.GetOrAdd(name, id);
         }
 
         /// <summary>
@@ -235,26 +235,26 @@ public ActorId CreateActorIdFromName(Type type, string name)
         /// optional <see cref="Event"/>. This event can only be used to access its payload,
         /// and cannot be handled.
         /// </summary>
-        public ActorId CreateActor(Type type, Event initialEvent = null, Guid opGroupId = default) =>
-            CreateActor(null, type, null, initialEvent, opGroupId);
+        public StateMachineId CreateStateMachine(Type type, Event initialEvent = null, Guid opGroupId = default) =>
+            CreateStateMachine(null, type, null, initialEvent, opGroupId);
 
         /// <summary>
         /// Creates a new state machine of the specified <see cref="Type"/> and name, and with the
         /// specified optional <see cref="Event"/>. This event can only be used to access
         /// its payload, and cannot be handled.
         /// </summary>
-        public ActorId CreateActor(Type type, string name, Event initialEvent = null, Guid opGroupId = default) =>
-            CreateActor(null, type, name, initialEvent, opGroupId);
+        public StateMachineId CreateStateMachine(Type type, string name, Event initialEvent = null, Guid opGroupId = default) =>
+            CreateStateMachine(null, type, name, initialEvent, opGroupId);
 
         /// <summary>
-        /// Creates a new state machine of the specified type, using the specified <see cref="ActorId"/>.
+        /// Creates a new state machine of the specified type, using the specified <see cref="StateMachineId"/>.
         /// This method optionally passes an <see cref="Event"/> to the new state machine, which can only
         /// be used to access its payload, and cannot be handled.
         /// </summary>
-        public ActorId CreateActor(ActorId id, Type type, Event initialEvent = null, Guid opGroupId = default)
+        public StateMachineId CreateStateMachine(StateMachineId id, Type type, Event initialEvent = null, Guid opGroupId = default)
         {
-            Assert(id != null, "Cannot create an actor using a null actor id.");
-            return CreateActor(id, type, null, initialEvent, opGroupId);
+            Assert(id != null, "Cannot create an state machine using a null state machine id.");
+            return CreateStateMachine(id, type, null, initialEvent, opGroupId);
         }
 
         /// <summary>
@@ -263,8 +263,8 @@ public ActorId CreateActor(ActorId id, Type type, Event initialEvent = null, Gui
         /// and cannot be handled. The method returns only when the state machine is initialized and
         /// the <see cref="Event"/> (if any) is handled.
         /// </summary>
-        public Task<ActorId> CreateActorAndExecuteAsync(Type type, Event e = null, Guid opGroupId = default) =>
-            CreateActorAndExecuteAsync(null, type, null, e, opGroupId);
+        public Task<StateMachineId> CreateStateMachineAndExecuteAsync(Type type, Event e = null, Guid opGroupId = default) =>
+            CreateStateMachineAndExecuteAsync(null, type, null, e, opGroupId);
 
         /// <summary>
         /// Creates a new state machine of the specified <see cref="Type"/> and name, and with the
@@ -272,8 +272,8 @@ public Task<ActorId> CreateActorAndExecuteAsync(Type type, Event e = null, Guid
         /// its payload, and cannot be handled. The method returns only when the state machine is
         /// initialized and the <see cref="Event"/> (if any) is handled.
         /// </summary>
-        public Task<ActorId> CreateActorAndExecuteAsync(Type type, string name, Event e = null, Guid opGroupId = default) =>
-            CreateActorAndExecuteAsync(null, type, name, e, opGroupId);
+        public Task<StateMachineId> CreateStateMachineAndExecuteAsync(Type type, string name, Event e = null, Guid opGroupId = default) =>
+            CreateStateMachineAndExecuteAsync(null, type, name, e, opGroupId);
 
         /// <summary>
         /// Creates a new state machine of the specified <see cref="Type"/>, using the specified unbound
@@ -282,43 +282,43 @@ public Task<ActorId> CreateActorAndExecuteAsync(Type type, string name, Event e
         /// the state machine is initialized and the <see cref="Event"/> (if any)
         /// is handled.
         /// </summary>
-        public Task<ActorId> CreateActorAndExecuteAsync(ActorId id, Type type, Event e = null, Guid opGroupId = default)
+        public Task<StateMachineId> CreateStateMachineAndExecuteAsync(StateMachineId id, Type type, Event e = null, Guid opGroupId = default)
         {
-            Assert(id != null, "Cannot create an actor using a null actor id.");
-            return CreateActorAndExecuteAsync(id, type, null, e, opGroupId);
+            Assert(id != null, "Cannot create an state machine using a null state machine id.");
+            return CreateStateMachineAndExecuteAsync(id, type, null, e, opGroupId);
         }
 
         /// <summary>
         /// Sends an asynchronous <see cref="Event"/> to a state machine.
         /// </summary>
-        public void SendEvent(ActorId targetId, Event e, Guid opGroupId = default)
+        public void SendEvent(StateMachineId targetId, Event e, Guid opGroupId = default)
         {
-            var senderOp = Scheduler.GetExecutingOperation<ActorOperation>();
-            SendEvent(targetId, e, senderOp?.Actor, opGroupId);
+            var senderOp = Scheduler.GetExecutingOperation<StateMachineOperation>();
+            SendEvent(targetId, e, senderOp?.StateMachine, opGroupId);
         }
 
         /// <summary>
         /// Sends an <see cref="Event"/> to a state machine. Returns immediately if the target was already
         /// running. Otherwise, blocks until the target handles the event and reaches quiescence.
         /// </summary>
-        public Task<bool> SendEventAndExecuteAsync(ActorId targetId, Event e, Guid opGroupId = default)
+        public Task<bool> SendEventAndExecuteAsync(StateMachineId targetId, Event e, Guid opGroupId = default)
         {
-            var senderOp = Scheduler.GetExecutingOperation<ActorOperation>();
-            return SendEventAndExecuteAsync(targetId, e, senderOp?.Actor, opGroupId);
+            var senderOp = Scheduler.GetExecutingOperation<StateMachineOperation>();
+            return SendEventAndExecuteAsync(targetId, e, senderOp?.StateMachine, opGroupId);
         }
 
         /// <summary>
         /// Returns the operation group id of the state machine with the specified id. Returns <see cref="Guid.Empty"/>
-        /// if the id is not set, or if the <see cref="ActorId"/> is not associated with this runtime. During
+        /// if the id is not set, or if the <see cref="StateMachineId"/> is not associated with this runtime. During
         /// testing, the runtime asserts that the specified state machine is currently executing.
         /// </summary>
-        public Guid GetCurrentOperationGroupId(ActorId currentActorId)
+        public Guid GetCurrentOperationGroupId(StateMachineId currentStateMachineId)
         {
-            var callerOp = Scheduler.GetExecutingOperation<ActorOperation>();
-            Assert(callerOp != null && currentActorId == callerOp.Actor.Id,
-                "Trying to access the operation group id of {0}, which is not the currently executing actor.",
-                currentActorId);
-            return callerOp.Actor.OperationGroupId;
+            var callerOp = Scheduler.GetExecutingOperation<StateMachineOperation>();
+            Assert(callerOp != null && currentStateMachineId == callerOp.StateMachine.Id,
+                "Trying to access the operation group id of {0}, which is not the currently executing state machine.",
+                currentStateMachineId);
+            return callerOp.StateMachine.OperationGroupId;
         }
 
         /// <summary>
@@ -346,7 +346,7 @@ internal void RunTest(Delegate testMethod, string testName)
 
                     OperationScheduler.StartOperation(op);
 
-                    if (testMethod is Action<IActorRuntime> actionWithRuntime)
+                    if (testMethod is Action<IStateMachineRuntime> actionWithRuntime)
                     {
                         actionWithRuntime(this);
                     }
@@ -354,7 +354,7 @@ internal void RunTest(Delegate testMethod, string testName)
                     {
                         action();
                     }
-                    else if (testMethod is Func<IActorRuntime, Tasks.Task> functionWithRuntime)
+                    else if (testMethod is Func<IStateMachineRuntime, Tasks.Task> functionWithRuntime)
                     {
                         await functionWithRuntime(this);
                     }
@@ -385,42 +385,42 @@ internal void RunTest(Delegate testMethod, string testName)
         }
 
         /// <summary>
-        /// Creates a new actor of the specified <see cref="Type"/> and name, using the specified
-        /// unbound actor id, and passes the specified optional <see cref="Event"/>. This event
+        /// Creates a new state machine of the specified <see cref="Type"/> and name, using the specified
+        /// unbound state machine id, and passes the specified optional <see cref="Event"/>. This event
         /// can only be used to access its payload, and cannot be handled.
         /// </summary>
-        internal ActorId CreateActor(ActorId id, Type type, string name, Event initialEvent = null,
+        internal StateMachineId CreateStateMachine(StateMachineId id, Type type, string name, Event initialEvent = null,
             Guid opGroupId = default)
         {
-            var creatorOp = Scheduler.GetExecutingOperation<ActorOperation>();
-            return CreateActor(id, type, name, initialEvent, creatorOp?.Actor, opGroupId);
+            var creatorOp = Scheduler.GetExecutingOperation<StateMachineOperation>();
+            return CreateStateMachine(id, type, name, initialEvent, creatorOp?.StateMachine, opGroupId);
         }
 
         /// <summary>
         /// Creates a new <see cref="StateMachine"/> of the specified <see cref="Type"/>.
         /// </summary>
-        internal ActorId CreateActor(ActorId id, Type type, string name, Event initialEvent, StateMachine creator,
+        internal StateMachineId CreateStateMachine(StateMachineId id, Type type, string name, Event initialEvent, StateMachine creator,
             Guid opGroupId)
         {
-            AssertExpectedCallerActor(creator, "CreateActor");
+            AssertExpectedCallerStateMachine(creator, "CreateStateMachine");
 
-            var actor = CreateActor(id, type, name, creator, opGroupId);
-            LogWriter.LogCreateStateMachine(actor.Id, creator?.Id.Name, creator?.Id.Type);
-            RunActorEventHandler(actor, initialEvent, true, null);
-            return actor.Id;
+            var stateMachine = CreateStateMachine(id, type, name, creator, opGroupId);
+            LogWriter.LogCreateStateMachine(stateMachine.Id, creator?.Id.Name, creator?.Id.Type);
+            RunStateMachineEventHandler(stateMachine, initialEvent, true, null);
+            return stateMachine.Id;
         }
 
         /// <summary>
-        /// Creates a new actor of the specified <see cref="Type"/> and name, using the specified
-        /// unbound actor id, and passes the specified optional <see cref="Event"/>. This event
+        /// Creates a new state machine of the specified <see cref="Type"/> and name, using the specified
+        /// unbound state machine id, and passes the specified optional <see cref="Event"/>. This event
         /// can only be used to access its payload, and cannot be handled. The method returns only
-        /// when the actor is initialized and the <see cref="Event"/> (if any) is handled.
+        /// when the state machine is initialized and the <see cref="Event"/> (if any) is handled.
         /// </summary>
-        internal Task<ActorId> CreateActorAndExecuteAsync(ActorId id, Type type, string name, Event initialEvent = null,
+        internal Task<StateMachineId> CreateStateMachineAndExecuteAsync(StateMachineId id, Type type, string name, Event initialEvent = null,
             Guid opGroupId = default)
         {
-            var creatorOp = Scheduler.GetExecutingOperation<ActorOperation>();
-            return CreateActorAndExecuteAsync(id, type, name, initialEvent, creatorOp?.Actor, opGroupId);
+            var creatorOp = Scheduler.GetExecutingOperation<StateMachineOperation>();
+            return CreateStateMachineAndExecuteAsync(id, type, name, initialEvent, creatorOp?.StateMachine, opGroupId);
         }
 
         /// <summary>
@@ -428,27 +428,27 @@ internal Task<ActorId> CreateActorAndExecuteAsync(ActorId id, Type type, string
         /// returns only when the state machine is initialized and the <see cref="Event"/> (if any)
         /// is handled.
         /// </summary>
-        internal async Task<ActorId> CreateActorAndExecuteAsync(ActorId id, Type type, string name,
+        internal async Task<StateMachineId> CreateStateMachineAndExecuteAsync(StateMachineId id, Type type, string name,
             Event initialEvent, StateMachine creator, Guid opGroupId)
         {
-            AssertExpectedCallerActor(creator, "CreateActorAndExecuteAsync");
-            Assert(creator != null, "Only an actor can call 'CreateActorAndExecuteAsync': avoid calling " +
-                                    "it directly from the test method; instead call it through a test driver actor.");
+            AssertExpectedCallerStateMachine(creator, "CreateStateMachineAndExecuteAsync");
+            Assert(creator != null, "Only a state machine can call 'CreateStateMachineAndExecuteAsync': avoid calling " +
+                                    "it directly from the test method; instead call it through a test driver state machine.");
 
-            var actor = CreateActor(id, type, name, creator, opGroupId);
-            RunActorEventHandler(actor, initialEvent, true, creator);
+            var stateMachine = CreateStateMachine(id, type, name, creator, opGroupId);
+            RunStateMachineEventHandler(stateMachine, initialEvent, true, creator);
 
-            // Wait until the actor reaches quiescence.
-            await creator.ReceiveEventAsync(typeof(QuiescentEvent), rev => (rev as QuiescentEvent).ActorId == actor.Id);
-            return await Task.FromResult(actor.Id);
+            // Wait until the state machine reaches quiescence.
+            await creator.ReceiveEventAsync(typeof(QuiescentEvent), rev => (rev as QuiescentEvent).StateMachineId == stateMachine.Id);
+            return await Task.FromResult(stateMachine.Id);
         }
 
         /// <summary>
         /// Creates a new state machine of the specified <see cref="Type"/>.
         /// </summary>
-        private StateMachine CreateActor(ActorId id, Type type, string name, StateMachine creator, Guid opGroupId)
+        private StateMachine CreateStateMachine(StateMachineId id, Type type, string name, StateMachine creator, Guid opGroupId)
         {
-            Assert(type.IsSubclassOf(typeof(StateMachine)), "Type '{0}' is not an actor.", type.FullName);
+            Assert(type.IsSubclassOf(typeof(StateMachine)), "Type '{0}' is not a state machine.", type.FullName);
 
             // Using ulong.MaxValue because a Create operation cannot specify
             // the id of its target, because the id does not exist yet.
@@ -457,42 +457,42 @@ private StateMachine CreateActor(ActorId id, Type type, string name, StateMachin
 
             if (id is null)
             {
-                id = new ActorId(type, name, this);
+                id = new StateMachineId(type, name, this);
             }
             else
             {
-                Assert(id.Runtime is null || id.Runtime == this, "Unbound actor id '{0}' was created by another runtime.", id.Value);
-                Assert(id.Type == type.FullName, "Cannot bind actor id '{0}' of type '{1}' to an actor of type '{2}'.",
+                Assert(id.Runtime is null || id.Runtime == this, "Unbound state machine id '{0}' was created by another runtime.", id.Value);
+                Assert(id.Type == type.FullName, "Cannot bind state machine id '{0}' of type '{1}' to an state machine of type '{2}'.",
                     id.Value, id.Type, type.FullName);
                 id.Bind(this);
             }
 
-            // The operation group id of the actor is set using the following precedence:
-            // (1) To the specified actor creation operation group id, if it is non-empty.
-            // (2) To the operation group id of the creator actor, if it exists and is non-empty.
+            // The operation group id of the state machine is set using the following precedence:
+            // (1) To the specified state machine creation operation group id, if it is non-empty.
+            // (2) To the operation group id of the creator state machine, if it exists and is non-empty.
             // (3) To the empty operation group id.
             if (opGroupId == Guid.Empty && creator != null)
             {
                 opGroupId = creator.OperationGroupId;
             }
 
-            var actor = Create(type);
-            IStateMachineManager stateMachineManager = new StateMachineManager(this, actor, opGroupId);
+            var stateMachine = Create(type);
+            IStateMachineManager stateMachineManager = new StateMachineManager(this, stateMachine, opGroupId);
 
-            IEventQueue eventQueue = new EventQueue(stateMachineManager, actor);
-            actor.Configure(this, id, stateMachineManager, eventQueue);
-            actor.SetupEventHandlers();
+            IEventQueue eventQueue = new EventQueue(stateMachineManager, stateMachine);
+            stateMachine.Configure(this, id, stateMachineManager, eventQueue);
+            stateMachine.SetupEventHandlers();
 
             if (CheckerConfiguration.ReportActivityCoverage)
             {
-                ReportActivityCoverageOfActor(actor);
+                ReportActivityCoverageOfStateMachine(stateMachine);
             }
 
-            var result = Scheduler.RegisterOperation(new ActorOperation(actor));
-            Assert(result, "Actor id '{0}' is used by an existing or previously halted actor.", id.Value);
+            var result = Scheduler.RegisterOperation(new StateMachineOperation(stateMachine));
+            Assert(result, "StateMachine id '{0}' is used by an existing or previously halted state machine.", id.Value);
             LogWriter.LogCreateStateMachine(id, creator?.Id.Name, creator?.Id.Type);
 
-            return actor;
+            return stateMachine;
         }
         
         /// <summary>
@@ -525,7 +525,7 @@ public static StateMachine Create(Type type)
         /// <summary>
         /// Sends an asynchronous <see cref="Event"/> to a state machine.
         /// </summary>
-        internal void SendEvent(ActorId targetId, Event e, StateMachine sender, Guid opGroupId)
+        internal void SendEvent(StateMachineId targetId, Event e, StateMachine sender, Guid opGroupId)
         {
             if (e is null)
             {
@@ -537,19 +537,19 @@ internal void SendEvent(ActorId targetId, Event e, StateMachine sender, Guid opG
 
             if (sender != null)
             {
-                Assert(targetId != null, "{0} is sending event {1} to a null actor.", sender.Id, e);
+                Assert(targetId != null, "{0} is sending event {1} to a null state machine.", sender.Id, e);
             }
             else
             {
-                Assert(targetId != null, "Cannot send event {1} to a null actor.", e);
+                Assert(targetId != null, "Cannot send event {1} to a null state machine.", e);
             }
 
-            AssertExpectedCallerActor(sender, "SendEvent");
+            AssertExpectedCallerStateMachine(sender, "SendEvent");
 
             var enqueueStatus = EnqueueEvent(targetId, e, sender, opGroupId, out var target);
             if (enqueueStatus is EnqueueStatus.EventHandlerNotRunning)
             {
-                RunActorEventHandler(target, null, false, null);
+                RunStateMachineEventHandler(target, null, false, null);
             }
         }
 
@@ -557,37 +557,37 @@ internal void SendEvent(ActorId targetId, Event e, StateMachine sender, Guid opG
         /// Sends an asynchronous <see cref="Event"/> to a state machine. Returns immediately if the target was
         /// already running. Otherwise, blocks until the target handles the event and reaches quiescence.
         /// </summary>
-        internal async Task<bool> SendEventAndExecuteAsync(ActorId targetId, Event e, StateMachine sender,
+        internal async Task<bool> SendEventAndExecuteAsync(StateMachineId targetId, Event e, StateMachine sender,
             Guid opGroupId)
         {
             Assert(e != null, "{0} is sending a null event.", sender.Id);
-            Assert(targetId != null, "{0} is sending event {1} to a null actor.", sender.Id, e);
-            AssertExpectedCallerActor(sender, "SendEventAndExecuteAsync");
+            Assert(targetId != null, "{0} is sending event {1} to a null state machine.", sender.Id, e);
+            AssertExpectedCallerStateMachine(sender, "SendEventAndExecuteAsync");
 
             var enqueueStatus = EnqueueEvent(targetId, e, sender, opGroupId, out var target);
             if (enqueueStatus is EnqueueStatus.EventHandlerNotRunning)
             {
-                RunActorEventHandler(target, null, false, sender);
+                RunStateMachineEventHandler(target, null, false, sender);
 
-                // Wait until the actor reaches quiescence.
-                await sender.ReceiveEventAsync(typeof(QuiescentEvent), rev => (rev as QuiescentEvent).ActorId == targetId);
+                // Wait until the state machine reaches quiescence.
+                await sender.ReceiveEventAsync(typeof(QuiescentEvent), rev => (rev as QuiescentEvent).StateMachineId == targetId);
                 return true;
             }
 
             // EnqueueStatus.EventHandlerNotRunning is not returned by EnqueueEvent
-            // (even when the actor was previously inactive) when the event e requires
-            // no action by the actor (i.e., it implicitly handles the event).
+            // (even when the state machine was previously inactive) when the event e requires
+            // no action by the state machine (i.e., it implicitly handles the event).
             return enqueueStatus is EnqueueStatus.Dropped || enqueueStatus is EnqueueStatus.NextEventUnavailable;
         }
 
         /// <summary>
-        /// Enqueues an event to the actor with the specified id.
+        /// Enqueues an event to the state machine with the specified id.
         /// </summary>
-        private EnqueueStatus EnqueueEvent(ActorId targetId, Event e, StateMachine sender, Guid opGroupId, out StateMachine target)
+        private EnqueueStatus EnqueueEvent(StateMachineId targetId, Event e, StateMachine sender, Guid opGroupId, out StateMachine target)
         {
-            target = Scheduler.GetOperationWithId<ActorOperation>(targetId.Value)?.Actor;
+            target = Scheduler.GetOperationWithId<StateMachineOperation>(targetId.Value)?.StateMachine;
             Assert(target != null,
-                "Cannot send event '{0}' to actor id '{1}' that is not bound to an actor instance.",
+                "Cannot send event '{0}' to state machine id '{1}' that is not bound to an state machine instance.",
                 e.GetType().FullName, targetId.Value);
 
             Scheduler.ScheduleNextEnabledOperation(AsyncOperationType.Send);
@@ -595,7 +595,7 @@ private EnqueueStatus EnqueueEvent(ActorId targetId, Event e, StateMachine sende
 
             // The operation group id of this operation is set using the following precedence:
             // (1) To the specified send operation group id, if it is non-empty.
-            // (2) To the operation group id of the sender actor, if it exists and is non-empty.
+            // (2) To the operation group id of the sender state machine, if it exists and is non-empty.
             // (3) To the empty operation group id.
             if (opGroupId == Guid.Empty && sender != null)
             {
@@ -644,9 +644,9 @@ private EnqueueStatus EnqueueEvent(StateMachine stateMachine, Event e, StateMach
         /// <param name="initialEvent">Optional event for initializing the state machine.</param>
         /// <param name="isFresh">If true, then this is a new state machine.</param>
         /// <param name="syncCaller">Caller state machine that is blocked for quiescence.</param>
-        private void RunActorEventHandler(StateMachine stateMachine, Event initialEvent, bool isFresh, StateMachine syncCaller)
+        private void RunStateMachineEventHandler(StateMachine stateMachine, Event initialEvent, bool isFresh, StateMachine syncCaller)
         {
-            var op = Scheduler.GetOperationWithId<ActorOperation>(stateMachine.Id.Value);
+            var op = Scheduler.GetOperationWithId<StateMachineOperation>(stateMachine.Id.Value);
             op.OnEnabled();
 
             var task = new Task(async () =>
@@ -678,7 +678,7 @@ private void RunActorEventHandler(StateMachine stateMachine, Event initialEvent,
                     Debug.WriteLine("<ScheduleDebug> Completed operation {0} on task '{1}'.", stateMachine.Id, Task.CurrentId);
                     op.OnCompleted();
 
-                    // The actor is inactive or halted, schedule the next enabled operation.
+                    // The state machine is inactive or halted, schedule the next enabled operation.
                     Scheduler.ScheduleNextEnabledOperation(AsyncOperationType.Stop);
                 }
                 catch (Exception ex)
@@ -835,27 +835,27 @@ public override void Assert(bool predicate, string s, params object[] args)
         }
 
         /// <summary>
-        /// Asserts that the actor calling an actor method is also
-        /// the actor that is currently executing.
+        /// Asserts that the state machine calling an state machine method is also
+        /// the state machine that is currently executing.
         /// </summary>
 #if !DEBUG
         [DebuggerHidden]
 #endif
-        private void AssertExpectedCallerActor(StateMachine caller, string calledAPI)
+        private void AssertExpectedCallerStateMachine(StateMachine caller, string calledAPI)
         {
             if (caller is null)
             {
                 return;
             }
 
-            var op = Scheduler.GetExecutingOperation<ActorOperation>();
+            var op = Scheduler.GetExecutingOperation<StateMachineOperation>();
             if (op is null)
             {
                 return;
             }
 
-            Assert(op.Actor.Equals(caller), "{0} invoked {1} on behalf of {2}.",
-                op.Actor.Id, calledAPI, caller.Id);
+            Assert(op.StateMachine.Equals(caller), "{0} invoked {1} on behalf of {2}.",
+                op.StateMachine.Id, calledAPI, caller.Id);
         }
 
         /// <summary>
@@ -888,7 +888,7 @@ internal void CheckNoMonitorInHotStateAtTermination()
         /// <inheritdoc/>
         internal override bool GetNondeterministicBooleanChoice(int maxValue, string callerName, string callerType)
         {
-            var caller = Scheduler.GetExecutingOperation<ActorOperation>()?.Actor;
+            var caller = Scheduler.GetExecutingOperation<StateMachineOperation>()?.StateMachine;
             if (caller != null)
             {
                 (caller.Manager as StateMachineManager).ProgramCounter++;
@@ -902,7 +902,7 @@ internal override bool GetNondeterministicBooleanChoice(int maxValue, string cal
         /// <inheritdoc/>
         internal override int GetNondeterministicIntegerChoice(int maxValue, string callerName, string callerType)
         {
-            var caller = Scheduler.GetExecutingOperation<ActorOperation>()?.Actor;
+            var caller = Scheduler.GetExecutingOperation<StateMachineOperation>()?.StateMachine;
             if (caller != null)
             {
                 (caller.Manager as StateMachineManager).ProgramCounter++;
@@ -914,13 +914,13 @@ internal override int GetNondeterministicIntegerChoice(int maxValue, string call
         }
         
         /// <summary>
-        /// Gets the actor of type <typeparamref name="TActor"/> with the specified id,
-        /// or null if no such actor exists.
+        /// Gets the state machine of type <typeparamref name="TStateMachine"/> with the specified id,
+        /// or null if no such state machine exists.
         /// </summary>
-        private TActor GetActorWithId<TActor>(ActorId id)
-            where TActor : StateMachine =>
+        private TStateMachine GetStateMachineWithId<TStateMachine>(StateMachineId id)
+            where TStateMachine : StateMachine =>
             id != null && StateMachineMap.TryGetValue(id, out var value) &&
-            value is TActor actor ? actor : null;
+            value is TStateMachine stateMachine ? stateMachine : null;
 
         /// <summary>
         /// Gets the <see cref="IAsyncOperation"/> that is executing on the current
@@ -957,18 +957,18 @@ internal void ScheduleNextOperation(AsyncOperationType type)
         /// <summary>
         /// Notifies that a state machine invoked an action.
         /// </summary>
-        internal void NotifyInvokedAction(StateMachine actor, MethodInfo action, string handlingStateName,
+        internal void NotifyInvokedAction(StateMachine stateMachine, MethodInfo action, string handlingStateName,
             string currentStateName, Event receivedEvent)
         {
-            LogWriter.LogExecuteAction(actor.Id, handlingStateName, currentStateName, action.Name);
+            LogWriter.LogExecuteAction(stateMachine.Id, handlingStateName, currentStateName, action.Name);
         }
 
         /// <summary>
         /// Notifies that a state machine dequeued an <see cref="Event"/>.
         /// </summary>
-        internal void NotifyDequeuedEvent(StateMachine actor, Event e, EventInfo eventInfo)
+        internal void NotifyDequeuedEvent(StateMachine stateMachine, Event e, EventInfo eventInfo)
         {
-            var op = Scheduler.GetOperationWithId<ActorOperation>(actor.Id.Value);
+            var op = Scheduler.GetOperationWithId<StateMachineOperation>(stateMachine.Id.Value);
 
             // Skip `ReceiveEventAsync` if the last operation exited the previous event handler,
             // to avoid scheduling duplicate `ReceiveEventAsync` operations.
@@ -979,27 +979,27 @@ internal void NotifyDequeuedEvent(StateMachine actor, Event e, EventInfo eventIn
             else
             {
                 Scheduler.ScheduleNextEnabledOperation(AsyncOperationType.Receive);
-                ResetProgramCounter(actor);
+                ResetProgramCounter(stateMachine);
             }
 
-            var stateName = actor.CurrentStateName;
-            LogWriter.LogDequeueEvent(actor.Id, stateName, e);
+            var stateName = stateMachine.CurrentStateName;
+            LogWriter.LogDequeueEvent(stateMachine.Id, stateName, e);
         }
 
         /// <summary>
         /// Notifies that a state machine dequeued the default <see cref="Event"/>.
         /// </summary>
-        internal void NotifyDefaultEventDequeued(StateMachine actor)
+        internal void NotifyDefaultEventDequeued(StateMachine stateMachine)
         {
             Scheduler.ScheduleNextEnabledOperation(AsyncOperationType.Receive);
-            ResetProgramCounter(actor);
+            ResetProgramCounter(stateMachine);
         }
 
         /// <summary>
         /// Notifies that the inbox of the specified state machine is about to be
         /// checked to see if the default event handler should fire.
         /// </summary>
-        internal void NotifyDefaultEventHandlerCheck(StateMachine actor)
+        internal void NotifyDefaultEventHandlerCheck(StateMachine stateMachine)
         {
             Scheduler.ScheduleNextEnabledOperation(AsyncOperationType.Default);
         }
@@ -1007,38 +1007,38 @@ internal void NotifyDefaultEventHandlerCheck(StateMachine actor)
         /// <summary>
         /// Notifies that a state machine raised an <see cref="Event"/>.
         /// </summary>
-        internal void NotifyRaisedEvent(StateMachine actor, Event e, EventInfo eventInfo)
+        internal void NotifyRaisedEvent(StateMachine stateMachine, Event e, EventInfo eventInfo)
         {
-            var stateName = actor.CurrentStateName;
-            LogWriter.LogRaiseEvent(actor.Id, stateName, e);
+            var stateName = stateMachine.CurrentStateName;
+            LogWriter.LogRaiseEvent(stateMachine.Id, stateName, e);
         }
 
         /// <summary>
         /// Notifies that a state machine is handling a raised <see cref="Event"/>.
         /// </summary>
-        internal void NotifyHandleRaisedEvent(StateMachine actor, Event e)
+        internal void NotifyHandleRaisedEvent(StateMachine stateMachine, Event e)
         {
-            var stateName = actor.CurrentStateName;
-            LogWriter.LogHandleRaisedEvent(actor.Id, stateName, e);
+            var stateName = stateMachine.CurrentStateName;
+            LogWriter.LogHandleRaisedEvent(stateMachine.Id, stateName, e);
         }
 
         /// <summary>
         /// Notifies that a state machine called <see cref="StateMachine.ReceiveEventAsync(Type[])"/>
         /// or one of its overloaded methods.
         /// </summary>
-        internal void NotifyReceiveCalled(StateMachine actor)
+        internal void NotifyReceiveCalled(StateMachine stateMachine)
         {
-            AssertExpectedCallerActor(actor, "ReceiveEventAsync");
+            AssertExpectedCallerStateMachine(stateMachine, "ReceiveEventAsync");
         }
 
         /// <summary>
         /// Notifies that a state machine enqueued an event that it was waiting to receive.
         /// </summary>
-        internal void NotifyReceivedEvent(StateMachine actor, Event e, EventInfo eventInfo)
+        internal void NotifyReceivedEvent(StateMachine stateMachine, Event e, EventInfo eventInfo)
         {
-            var stateName = actor.CurrentStateName;
-            LogWriter.LogReceiveEvent(actor.Id, stateName, e, wasBlocked: true);
-            var op = Scheduler.GetOperationWithId<ActorOperation>(actor.Id.Value);
+            var stateName = stateMachine.CurrentStateName;
+            LogWriter.LogReceiveEvent(stateMachine.Id, stateName, e, wasBlocked: true);
+            var op = Scheduler.GetOperationWithId<StateMachineOperation>(stateMachine.Id.Value);
             op.OnReceivedEvent();
         }
 
@@ -1046,20 +1046,20 @@ internal void NotifyReceivedEvent(StateMachine actor, Event e, EventInfo eventIn
         /// Notifies that a state machine received an event without waiting because the event
         /// was already in the inbox when the state machine invoked the receiving statement.
         /// </summary>
-        internal void NotifyReceivedEventWithoutWaiting(StateMachine actor, Event e, EventInfo eventInfo)
+        internal void NotifyReceivedEventWithoutWaiting(StateMachine stateMachine, Event e, EventInfo eventInfo)
         {
-            var stateName = actor.CurrentStateName;
-            LogWriter.LogReceiveEvent(actor.Id, stateName, e, wasBlocked: false);
+            var stateName = stateMachine.CurrentStateName;
+            LogWriter.LogReceiveEvent(stateMachine.Id, stateName, e, wasBlocked: false);
             Scheduler.ScheduleNextEnabledOperation(AsyncOperationType.Receive);
-            ResetProgramCounter(actor);
+            ResetProgramCounter(stateMachine);
         }
 
         /// <summary>
         /// Notifies that a state machine is waiting for the specified task to complete.
         /// </summary>
-        internal void NotifyWaitTask(StateMachine actor, Task task)
+        internal void NotifyWaitTask(StateMachine stateMachine, Task task)
         {
-            Assert(task != null, "{0} is waiting for a null task to complete.", actor.Id);
+            Assert(task != null, "{0} is waiting for a null task to complete.", stateMachine.Id);
 
             var finished = task.IsCompleted || task.IsCanceled || task.IsFaulted;
             if (!finished)
@@ -1067,7 +1067,7 @@ internal void NotifyWaitTask(StateMachine actor, Task task)
                 Assert(finished,
                     "Controlled task '{0}' is trying to wait for an uncontrolled task or awaiter to complete. Please " +
                     "make sure to avoid using concurrency APIs (e.g. 'Task.Run', 'Task.Delay' or 'Task.Yield' from " +
-                    "the 'System.Threading.Tasks' namespace) inside actor handlers. If you are using external libraries " +
+                    "the 'System.Threading.Tasks' namespace) inside state machine handlers. If you are using external libraries " +
                     "that are executing concurrently, you will need to mock them during testing.",
                     Task.CurrentId);
             }
@@ -1076,24 +1076,24 @@ internal void NotifyWaitTask(StateMachine actor, Task task)
         /// <summary>
         /// Notifies that a state machine is waiting to receive an event of one of the specified types.
         /// </summary>
-        internal void NotifyWaitEvent(StateMachine actor, IEnumerable<Type> eventTypes)
+        internal void NotifyWaitEvent(StateMachine stateMachine, IEnumerable<Type> eventTypes)
         {
-            var stateName = actor.CurrentStateName;
-            var op = Scheduler.GetOperationWithId<ActorOperation>(actor.Id.Value);
+            var stateName = stateMachine.CurrentStateName;
+            var op = Scheduler.GetOperationWithId<StateMachineOperation>(stateMachine.Id.Value);
             op.OnWaitEvent(eventTypes);
 
             var eventWaitTypesArray = eventTypes.ToArray();
             if (eventWaitTypesArray.Length == 1)
             {
-                LogWriter.LogWaitEvent(actor.Id, stateName, eventWaitTypesArray[0]);
+                LogWriter.LogWaitEvent(stateMachine.Id, stateName, eventWaitTypesArray[0]);
             }
             else
             {
-                LogWriter.LogWaitEvent(actor.Id, stateName, eventWaitTypesArray);
+                LogWriter.LogWaitEvent(stateMachine.Id, stateName, eventWaitTypesArray);
             }
 
             Scheduler.ScheduleNextEnabledOperation(AsyncOperationType.Join);
-            ResetProgramCounter(actor);
+            ResetProgramCounter(stateMachine);
         }
 
         /// <summary>
@@ -1181,7 +1181,7 @@ internal void NotifyMonitorError(Monitor monitor)
         /// <summary>
         /// Tries to handle the specified dropped <see cref="Event"/>.
         /// </summary>
-        internal void TryHandleDroppedEvent(Event e, ActorId id) => OnEventDropped?.Invoke(e, id);
+        internal void TryHandleDroppedEvent(Event e, StateMachineId id) => OnEventDropped?.Invoke(e, id);
         
         /// <inheritdoc/>
         public override TextWriter SetLogger(TextWriter logger) => LogWriter.SetLogger(logger);
@@ -1193,14 +1193,14 @@ internal void NotifyMonitorError(Monitor monitor)
         public void SetJsonLogger(JsonWriter jsonLogger) => LogWriter.SetJsonLogger(jsonLogger);
         
         /// <summary>
-        /// Use this method to register an <see cref="IActorRuntimeLog"/>.
+        /// Use this method to register an <see cref="IStateMachineRuntimeLog"/>.
         /// </summary>
-        public void RegisterLog(IActorRuntimeLog log) => LogWriter.RegisterLog(log);
+        public void RegisterLog(IStateMachineRuntimeLog log) => LogWriter.RegisterLog(log);
 
         /// <summary>
-        /// Use this method to unregister a previously registered <see cref="IActorRuntimeLog"/>.
+        /// Use this method to unregister a previously registered <see cref="IStateMachineRuntimeLog"/>.
         /// </summary>
-        public void RemoveLog(IActorRuntimeLog log) => LogWriter.RemoveLog(log);
+        public void RemoveLog(IStateMachineRuntimeLog log) => LogWriter.RemoveLog(log);
 
         /// <summary>
         /// Get the coverage graph information (if any). This information is only available
@@ -1212,13 +1212,13 @@ public CoverageInfo GetCoverageInfo()
             var result = CoverageInfo;
             if (result != null)
             {
-                var builder = LogWriter.GetLogsOfType<ActorRuntimeLogGraphBuilder>().FirstOrDefault();
+                var builder = LogWriter.GetLogsOfType<StateMachineRuntimeLogGraphBuilder>().FirstOrDefault();
                 if (builder != null)
                 {
                     result.CoverageGraph = builder.SnapshotGraph(CheckerConfiguration.IsDgmlBugGraph);
                 }
 
-                var eventCoverage = LogWriter.GetLogsOfType<ActorRuntimeLogEventCoverage>().FirstOrDefault();
+                var eventCoverage = LogWriter.GetLogsOfType<StateMachineRuntimeLogEventCoverage>().FirstOrDefault();
                 if (eventCoverage != null)
                 {
                     result.EventInfo = eventCoverage.EventCoverage;
@@ -1229,25 +1229,25 @@ public CoverageInfo GetCoverageInfo()
         }
 
         /// <summary>
-        /// Reports actors that are to be covered in coverage report.
+        /// Reports state machines that are to be covered in coverage report.
         /// </summary>
-        private void ReportActivityCoverageOfActor(StateMachine actor)
+        private void ReportActivityCoverageOfStateMachine(StateMachine stateMachine)
         {
-            var name = actor.GetType().FullName;
+            var name = stateMachine.GetType().FullName;
             if (CoverageInfo.IsMachineDeclared(name))
             {
                 return;
             }
         
             // Fetch states.
-            var states = actor.GetAllStates();
+            var states = stateMachine.GetAllStates();
             foreach (var state in states)
             {
                 CoverageInfo.DeclareMachineState(name, state);
             }
 
             // Fetch registered events.
-            var pairs = actor.GetAllStateEventPairs();
+            var pairs = stateMachine.GetAllStateEventPairs();
             foreach (var tup in pairs)
             {
                 CoverageInfo.DeclareStateEvent(name, tup.Item1, tup.Item2);
@@ -1283,13 +1283,13 @@ private void ReportActivityCoverageOfMonitor(Monitor monitor)
         }
 
         /// <summary>
-        /// Resets the program counter of the specified actor.
+        /// Resets the program counter of the specified stateMachine.
         /// </summary>
-        private static void ResetProgramCounter(StateMachine actor)
+        private static void ResetProgramCounter(StateMachine stateMachine)
         {
-            if (actor != null)
+            if (stateMachine != null)
             {
-                (actor.Manager as StateMachineManager).ProgramCounter = 0;
+                (stateMachine.Manager as StateMachineManager).ProgramCounter = 0;
             }
         }
 
@@ -1306,9 +1306,9 @@ internal int GetProgramState()
 
                 foreach (var operation in Scheduler.GetRegisteredOperations().OrderBy(op => op.Id))
                 {
-                    if (operation is ActorOperation actorOperation)
+                    if (operation is StateMachineOperation stateMachineOperation)
                     {
-                        hash *= 31 + actorOperation.Actor.GetHashedState();
+                        hash *= 31 + stateMachineOperation.StateMachine.GetHashedState();
                     }
                 }
 
@@ -1336,7 +1336,7 @@ internal override void WrapAndThrowException(Exception exception, string s, para
         }
 
         /// <summary>
-        /// Waits until all actors have finished execution.
+        /// Waits until all stateMachines have finished execution.
         /// </summary>
         [DebuggerStepThrough]
         internal async Task WaitAsync()
diff --git a/Src/PChecker/CheckerCore/SystematicTesting/OperationScheduler.cs b/Src/PChecker/CheckerCore/SystematicTesting/OperationScheduler.cs
index e21e6770e..718118e5f 100644
--- a/Src/PChecker/CheckerCore/SystematicTesting/OperationScheduler.cs
+++ b/Src/PChecker/CheckerCore/SystematicTesting/OperationScheduler.cs
@@ -477,7 +477,7 @@ internal void CheckNoExternalConcurrencyUsed()
                 NotifyAssertionFailure(string.Format(CultureInfo.InvariantCulture,
                     "Uncontrolled task '{0}' invoked a runtime method. Please make sure to avoid using concurrency APIs " +
                     "(e.g. 'Task.Run', 'Task.Delay' or 'Task.Yield' from the 'System.Threading.Tasks' namespace) inside " +
-                    "actor handlers or controlled tasks. If you are using external libraries that are executing concurrently, " +
+                    "state machine handlers or controlled tasks. If you are using external libraries that are executing concurrently, " +
                     "you will need to mock them during testing.",
                     Task.CurrentId.HasValue ? Task.CurrentId.Value.ToString() : "<unknown>"));
             }
diff --git a/Src/PChecker/CheckerCore/SystematicTesting/Operations/ActorOperation.cs b/Src/PChecker/CheckerCore/SystematicTesting/Operations/StateMachineOperation.cs
similarity index 78%
rename from Src/PChecker/CheckerCore/SystematicTesting/Operations/ActorOperation.cs
rename to Src/PChecker/CheckerCore/SystematicTesting/Operations/StateMachineOperation.cs
index af9d103e3..7bd7d2837 100644
--- a/Src/PChecker/CheckerCore/SystematicTesting/Operations/ActorOperation.cs
+++ b/Src/PChecker/CheckerCore/SystematicTesting/Operations/StateMachineOperation.cs
@@ -4,31 +4,31 @@
 using System;
 using System.Collections.Generic;
 using System.Diagnostics;
-using PChecker.Actors;
+using PChecker.StateMachines;
 
 namespace PChecker.SystematicTesting.Operations
 {
     /// <summary>
-    /// Contains information about an asynchronous actor operation
+    /// Contains information about an asynchronous state machine operation
     /// that can be controlled during testing.
     /// </summary>
     [DebuggerStepThrough]
-    internal sealed class ActorOperation : AsyncOperation
+    internal sealed class StateMachineOperation : AsyncOperation
     {
         /// <summary>
-        /// The actor that executes this operation.
+        /// The state machine that executes this operation.
         /// </summary>
-        internal readonly StateMachine Actor;
+        internal readonly StateMachine StateMachine;
 
         /// <summary>
         /// Unique id of the operation.
         /// </summary>
-        public override ulong Id => Actor.Id.Value;
+        public override ulong Id => StateMachine.Id.Value;
 
         /// <summary>
         /// Unique name of the operation.
         /// </summary>
-        public override string Name => Actor.Id.Name;
+        public override string Name => StateMachine.Id.Name;
 
         /// <summary>
         /// Set of events that this operation is waiting to receive. Receiving
@@ -44,12 +44,12 @@ internal sealed class ActorOperation : AsyncOperation
         internal bool SkipNextReceiveSchedulingPoint;
 
         /// <summary>
-        /// Initializes a new instance of the <see cref="ActorOperation"/> class.
+        /// Initializes a new instance of the <see cref="StateMachineOperation"/> class.
         /// </summary>
-        internal ActorOperation(StateMachine actor)
+        internal StateMachineOperation(StateMachine stateMachine)
             : base()
         {
-            Actor = actor;
+            StateMachine = stateMachine;
             EventDependencies = new HashSet<Type>();
             SkipNextReceiveSchedulingPoint = false;
         }
diff --git a/Src/PChecker/CheckerCore/SystematicTesting/TestMethodInfo.cs b/Src/PChecker/CheckerCore/SystematicTesting/TestMethodInfo.cs
index c7df5035c..0a7e1e6cb 100644
--- a/Src/PChecker/CheckerCore/SystematicTesting/TestMethodInfo.cs
+++ b/Src/PChecker/CheckerCore/SystematicTesting/TestMethodInfo.cs
@@ -6,7 +6,7 @@
 using System.Linq;
 using System.Reflection;
 using System.Runtime.CompilerServices;
-using PChecker.Actors;
+using PChecker.StateMachines;
 using PChecker.IO.Debugging;
 using PChecker.Runtime;
 using PChecker.Tasks;
@@ -164,10 +164,10 @@ private static (Delegate testMethod, string testName) GetTestMethod(Assembly ass
                                      testMethod.GetCustomAttribute(typeof(AsyncStateMachineAttribute)) != null;
 
             var hasNoInputParameters = testParams.Length is 0;
-            var hasActorInputParameters = testParams.Length is 1 && testParams[0].ParameterType == typeof(IActorRuntime);
+            var hasStateMachineInputParameters = testParams.Length is 1 && testParams[0].ParameterType == typeof(IStateMachineRuntime);
             var hasTaskInputParameters = testParams.Length is 1 && testParams[0].ParameterType == typeof(ICoyoteRuntime);
 
-            if (!((hasVoidReturnType || hasAsyncReturnType) && (hasNoInputParameters || hasActorInputParameters || hasTaskInputParameters) &&
+            if (!((hasVoidReturnType || hasAsyncReturnType) && (hasNoInputParameters || hasStateMachineInputParameters || hasTaskInputParameters) &&
                   !testMethod.IsAbstract && !testMethod.IsVirtual && !testMethod.IsConstructor &&
                   !testMethod.ContainsGenericParameters && testMethod.IsPublic && testMethod.IsStatic))
             {
@@ -178,21 +178,21 @@ private static (Delegate testMethod, string testName) GetTestMethod(Assembly ass
                                     $"  [{typeof(TestAttribute).FullName}]\n" +
                                     $"  public static void {testMethod.Name}(ICoyoteRuntime runtime) {{ ... }}\n\n" +
                                     $"  [{typeof(TestAttribute).FullName}]\n" +
-                                    $"  public static void {testMethod.Name}(IActorRuntime runtime) {{ ... }}\n\n" +
+                                    $"  public static void {testMethod.Name}(IStateMachineRuntime runtime) {{ ... }}\n\n" +
                                     $"  [{typeof(TestAttribute).FullName}]\n" +
                                     $"  public static async {typeof(Task).FullName} {testMethod.Name}() {{ ... await ... }}\n\n" +
                                     $"  [{typeof(TestAttribute).FullName}]\n" +
                                     $"  public static async {typeof(Task).FullName} {testMethod.Name}(ICoyoteRuntime runtime) {{ ... await ... }}\n\n" +
                                     $"  [{typeof(TestAttribute).FullName}]\n" +
-                                    $"  public static async {typeof(Task).FullName} {testMethod.Name}(IActorRuntime runtime) {{ ... await ... }}");
+                                    $"  public static async {typeof(Task).FullName} {testMethod.Name}(IStateMachineRuntime runtime) {{ ... await ... }}");
             }
 
             Delegate test;
             if (hasAsyncReturnType)
             {
-                if (hasActorInputParameters)
+                if (hasStateMachineInputParameters)
                 {
-                    test = Delegate.CreateDelegate(typeof(Func<IActorRuntime, Task>), testMethod);
+                    test = Delegate.CreateDelegate(typeof(Func<IStateMachineRuntime, Task>), testMethod);
                 }
                 else if (hasTaskInputParameters)
                 {
@@ -205,9 +205,9 @@ private static (Delegate testMethod, string testName) GetTestMethod(Assembly ass
             }
             else
             {
-                if (hasActorInputParameters)
+                if (hasStateMachineInputParameters)
                 {
-                    test = Delegate.CreateDelegate(typeof(Action<IActorRuntime>), testMethod);
+                    test = Delegate.CreateDelegate(typeof(Action<IStateMachineRuntime>), testMethod);
                 }
                 else if (hasTaskInputParameters)
                 {
diff --git a/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs b/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs
index 84463cc24..a18300000 100644
--- a/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs
+++ b/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs
@@ -14,8 +14,8 @@
 using System.Threading;
 using System.Threading.Tasks;
 using System.Xml;
-using PChecker.Actors;
-using PChecker.Actors.Logging;
+using PChecker.StateMachines;
+using PChecker.StateMachines.Logging;
 using PChecker.Coverage;
 using PChecker.IO;
 using PChecker.IO.Debugging;
@@ -133,7 +133,7 @@ public override void Write(Utf8JsonWriter writer, Encoding value, JsonSerializer
         public TestReport TestReport { get; set; }
 
         /// <summary>
-        /// A graph of the actors, state machines and events of a single test schedule.
+        /// A graph of the state machines, state machines and events of a single test schedule.
         /// </summary>
         private Graph Graph;
 
@@ -223,7 +223,7 @@ public static TestingEngine Create(CheckerConfiguration checkerConfiguration, Ac
         /// <summary>
         /// Creates a new systematic testing engine.
         /// </summary>
-        public static TestingEngine Create(CheckerConfiguration checkerConfiguration, Action<IActorRuntime> test) =>
+        public static TestingEngine Create(CheckerConfiguration checkerConfiguration, Action<IStateMachineRuntime> test) =>
             new TestingEngine(checkerConfiguration, test);
 
         /// <summary>
@@ -241,7 +241,7 @@ public static TestingEngine Create(CheckerConfiguration checkerConfiguration, Fu
         /// <summary>
         /// Creates a new systematic testing engine.
         /// </summary>
-        public static TestingEngine Create(CheckerConfiguration checkerConfiguration, Func<IActorRuntime, Task> test) =>
+        public static TestingEngine Create(CheckerConfiguration checkerConfiguration, Func<IStateMachineRuntime, Task> test) =>
             new TestingEngine(checkerConfiguration, test);
 
         /// <summary>
@@ -381,7 +381,7 @@ public void Run()
                     }
 
 
-                    Error.ReportAndExit("Exception thrown during testing outside the context of an actor, " +
+                    Error.ReportAndExit("Exception thrown during testing outside the context of an state machine, " +
                                         "possibly in a test method. Please use /debug /v:2 to print more information.");
                 }
             }
@@ -778,9 +778,9 @@ public void RegisterPerIterationCallBack(Action<int> callback)
         /// </summary>
         private void InitializeCustomLogging(ControlledRuntime runtime)
         {
-            if (!string.IsNullOrEmpty(_checkerConfiguration.CustomActorRuntimeLogType))
+            if (!string.IsNullOrEmpty(_checkerConfiguration.CustomStateMachineRuntimeLogType))
             {
-                var log = Activate<IActorRuntimeLog>(_checkerConfiguration.CustomActorRuntimeLogType);
+                var log = Activate<IStateMachineRuntimeLog>(_checkerConfiguration.CustomStateMachineRuntimeLogType);
                 if (log != null)
                 {
                     runtime.RegisterLog(log);
@@ -790,7 +790,7 @@ private void InitializeCustomLogging(ControlledRuntime runtime)
             if (_checkerConfiguration.IsDgmlGraphEnabled || _checkerConfiguration.ReportActivityCoverage)
             {
                 // Registers an activity coverage graph builder.
-                runtime.RegisterLog(new ActorRuntimeLogGraphBuilder(false)
+                runtime.RegisterLog(new StateMachineRuntimeLogGraphBuilder(false)
                 {
                     CollapseMachineInstances = _checkerConfiguration.ReportActivityCoverage
                 });
@@ -799,7 +799,7 @@ private void InitializeCustomLogging(ControlledRuntime runtime)
             if (_checkerConfiguration.ReportActivityCoverage)
             {
                 // Need this additional logger to get the event coverage report correct
-                runtime.RegisterLog(new ActorRuntimeLogEventCoverage());
+                runtime.RegisterLog(new StateMachineRuntimeLogEventCoverage());
             }
 
             if (_checkerConfiguration.IsXmlLogEnabled)
diff --git a/Src/PChecker/CheckerCore/SystematicTesting/Traces/ScheduleStep.cs b/Src/PChecker/CheckerCore/SystematicTesting/Traces/ScheduleStep.cs
index 59acffd09..ad1f5b936 100644
--- a/Src/PChecker/CheckerCore/SystematicTesting/Traces/ScheduleStep.cs
+++ b/Src/PChecker/CheckerCore/SystematicTesting/Traces/ScheduleStep.cs
@@ -49,14 +49,14 @@ internal sealed class ScheduleStep
         /// <summary>
         /// Creates a schedule step.
         /// </summary>
-        internal static ScheduleStep CreateSchedulingChoice(int index, ulong scheduledActorId)
+        internal static ScheduleStep CreateSchedulingChoice(int index, ulong scheduledStateMachineId)
         {
             var scheduleStep = new ScheduleStep();
 
             scheduleStep.Index = index;
             scheduleStep.Type = ScheduleStepType.SchedulingChoice;
 
-            scheduleStep.ScheduledOperationId = scheduledActorId;
+            scheduleStep.ScheduledOperationId = scheduledStateMachineId;
 
             scheduleStep.BooleanChoice = null;
             scheduleStep.IntegerChoice = null;
diff --git a/Src/PChecker/CheckerCore/SystematicTesting/Traces/ScheduleTrace.cs b/Src/PChecker/CheckerCore/SystematicTesting/Traces/ScheduleTrace.cs
index f4db75429..c039f6673 100644
--- a/Src/PChecker/CheckerCore/SystematicTesting/Traces/ScheduleTrace.cs
+++ b/Src/PChecker/CheckerCore/SystematicTesting/Traces/ScheduleTrace.cs
@@ -78,9 +78,9 @@ internal ScheduleTrace(string[] traceDump)
         /// <summary>
         /// Adds a scheduling choice.
         /// </summary>
-        internal void AddSchedulingChoice(ulong scheduledActorId)
+        internal void AddSchedulingChoice(ulong scheduledStateMachineId)
         {
-            var scheduleStep = ScheduleStep.CreateSchedulingChoice(Count, scheduledActorId);
+            var scheduleStep = ScheduleStep.CreateSchedulingChoice(Count, scheduledStateMachineId);
             Push(scheduleStep);
         }
 
diff --git a/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs b/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs
index 181e3a80b..242409b16 100644
--- a/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs
+++ b/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs
@@ -119,7 +119,7 @@ private void WriteInitializeInterfaces(CompilationContext context, StringWriter
             {
                 context.WriteLine(output, $"public class {context.Names.GetNameForDecl(iface)} : PMachineValue {{");
                 context.WriteLine(output,
-                    $"public {context.Names.GetNameForDecl(iface)} (ActorId machine, List<string> permissions) : base(machine, permissions) {{ }}");
+                    $"public {context.Names.GetNameForDecl(iface)} (StateMachineId machine, List<string> permissions) : base(machine, permissions) {{ }}");
                 context.WriteLine(output, "}");
                 context.WriteLine(output);
             }
@@ -150,8 +150,8 @@ private void WriteInitializeInterfaces(CompilationContext context, StringWriter
         private void WriteSourcePrologue(CompilationContext context, StringWriter output)
         {
             context.WriteLine(output, "using PChecker;");
-            context.WriteLine(output, "using PChecker.Actors;");
-            context.WriteLine(output, "using PChecker.Actors.Events;");
+            context.WriteLine(output, "using PChecker.StateMachines;");
+            context.WriteLine(output, "using PChecker.StateMachines.Events;");
             context.WriteLine(output, "using PChecker.Runtime;");
             context.WriteLine(output, "using PChecker.Specifications;");
             context.WriteLine(output, "using System;");
@@ -385,7 +385,7 @@ private void WriteTestFunction(CompilationContext context, StringWriter output,
         {
             context.WriteLine(output);
             context.WriteLine(output, "[PChecker.SystematicTesting.Test]");
-            context.WriteLine(output, "public static void Execute(IActorRuntime runtime) {");
+            context.WriteLine(output, "public static void Execute(IStateMachineRuntime runtime) {");
             context.WriteLine(output, "runtime.RegisterLog(new PLogFormatter());");
             context.WriteLine(output, "runtime.RegisterLog(new PJsonFormatter());");
             context.WriteLine(output, "PModule.runtime = runtime;");
@@ -396,7 +396,7 @@ private void WriteTestFunction(CompilationContext context, StringWriter output,
             context.WriteLine(output, "InitializeMonitorMap(runtime);");
             context.WriteLine(output, "InitializeMonitorObserves();");
             context.WriteLine(output,
-                $"runtime.CreateActor(typeof(_GodMachine), new _GodMachine.Config(typeof({main})));");
+                $"runtime.CreateStateMachine(typeof(_GodMachine), new _GodMachine.Config(typeof({main})));");
             context.WriteLine(output, "}");
         }
 
@@ -418,7 +418,7 @@ private void WriteInitializeMonitorMap(CompilationContext context, StringWriter
                 }
             }
 
-            context.WriteLine(output, "public static void InitializeMonitorMap(IActorRuntime runtime) {");
+            context.WriteLine(output, "public static void InitializeMonitorMap(IStateMachineRuntime runtime) {");
             context.WriteLine(output, "PModule.monitorMap.Clear();");
             foreach (var machine in machineMap)
             {
diff --git a/Src/PCompiler/CompilerCore/Backend/CSharp/Constants.cs b/Src/PCompiler/CompilerCore/Backend/CSharp/Constants.cs
index 595f3073e..b63f3cd46 100644
--- a/Src/PCompiler/CompilerCore/Backend/CSharp/Constants.cs
+++ b/Src/PCompiler/CompilerCore/Backend/CSharp/Constants.cs
@@ -26,7 +26,7 @@ internal class Constants
 using System;
 using System.IO;
 using System.Linq;
-using PChecker.Actors;
+using PChecker.StateMachines;
 
 namespace PImplementation
 {
@@ -39,7 +39,7 @@ public static void Main(string[] args)
             // update the path to the schedule file.
             string schedule = File.ReadAllText(""absolute path to *.schedule file"");
             configuration.WithReplayStrategy(schedule);
-            TestingEngine engine = TestingEngine.Create(configuration, (Action<IActorRuntime>)PImplementation.<Name of the test case>.Execute);
+            TestingEngine engine = TestingEngine.Create(configuration, (Action<IStateMachineRuntime>)PImplementation.<Name of the test case>.Execute);
             engine.Run();
             string bug = engine.TestReport.BugReports.FirstOrDefault();
                 if (bug != null)
diff --git a/Src/PCompiler/CompilerCore/Backend/Java/TypeManager.cs b/Src/PCompiler/CompilerCore/Backend/Java/TypeManager.cs
index b06f3a266..75ec9954c 100644
--- a/Src/PCompiler/CompilerCore/Backend/Java/TypeManager.cs
+++ b/Src/PCompiler/CompilerCore/Backend/Java/TypeManager.cs
@@ -179,7 +179,7 @@ internal static string ToJavaLiteral(string s)
 
             internal class JMachine : JType
             {
-                // Source/CheckerCore/Actors/ActorId.cs stores ActorID values as ulongs
+                // Source/CheckerCore/StateMachines/StateMachineId.cs stores StateMachineID values as ulongs
 
                 internal JMachine()
                 {