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.


This site is temporarily in read only mode and not accepting new answers.

Browse other questions tagged .