2
$\begingroup$

Here is a simple transition system of beverage vending machine: beverage vending machine

The exemplary execution fragments can look like this:

enter image description here

Now, imagine we have multi-process TS where processes are identical and communicate over channels. I don't understand the semantics of how to present an execution fragment that runs across multiple processes. Should I specify the whole execution in one line? If yes how do I denote that the state belongs to some certain process? Or maybe I present execution fragment on each process in the separate line? I'd love to see a "meta-example" of how that could look like.

I am referring to this specific exercise sheet, task 3.) b). The figures are from the book "Principles of Model Checking" by Christel Baier and Joost-Pieter Katoen p. 22 and p. 25.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.