Guarded Protocols

In this chapter we extend the computational model of Section 2.2 with a new means of coordination. Until now processes coordinated with synchronized transitions and we have used transition labels to express which transitions should be taken together. In this chapter, we introduce guards, which are conditions on the global state and determine whether a specific local transition may be fired. We review results on systems with guards that contain quantifiers over all processes except the one evaluating the guard. Hence, the current state of other processes may restrict the control flow of a process. In contrast to synchronized transitions that, intuitively, link transitions of different processes, guards link transitions to the state of other processes.

Authors and Affiliations

1. Graz University of Technology, Austria

   Roderick Bloem, Ayrat Khalimov & Swen Jacobs

2. Saarland University, Saarbrücken, Germany

   Swen Jacobs

3. Vienna University of Technology, Austria

   Igor Konnov, Helmut Veith & Josef Widder

4. University of Naples “Federico II”, Italy

   Sasha Rubin

Reprints and permissions

© 2015 Springer Nature Switzerland AG

Policies and ethics