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.


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.