-simulation kernel[^kernel]. When an actor needs to interact with the simulation
-kernel (eg. to start a communication), it issues a <i>simcall</i>
-(simulation call, an analogy to system calls) to the simulation kernel.
-This freezes the actor until it is woken up by the simulation kernel
-(eg. when the communication is finished).
-
-The key ideas here are:
+simulation kernel. The interactions between these actors and the
+simulation kernel are very similar to the ones between the system
+processes and the Operating System (except that the actors and
+simulation kernel share the same address space in a single OS
+process).
+
+When an actor needs to interact with the outer world (eg. to start a
+communication), it issues a <i>simcall</i> (simulation call), just
+like a system process issues a <i>syscall</i> to interact with its
+environment through the Operating System. Any <i>simcall</i> freezes
+the actor until it is woken up by the simulation kernel (eg. when the
+communication is finished).
+
+Mimicking the OS behavior may seem over-engineered here, but this is
+mandatory to the model-checker. The simcalls, representing actors'
+actions, are the transitions of the formal system. Verifying the
+system requires to manipulate these transitions explicitly. This also
+allows to run safely the actors in parallel, even if this is less
+commonly used by our users.
+
+So, the key ideas here are: