State Properties

  • Wolfgang Reisig


Important properties of a system pertain to the system’s reachable states. In a system net N, those are the reachable markings. We represent such a state property E of N with an expression a that contains as variables the places of N. If, for a marking M, each place p in a is then replaced with M(p), the expression can be evaluated to either true (“E holds in M”) or false (“E does not hold in M”).

State properties are often expressed as linear equations or inequalities. This chapter covers the form and the validity of such equations and inequalities. How to prove their validity is covered in the following chapters. As an example, we start out with properties of the cookie vending machine. The form of linear equations and inequalities is very simple and is explained in the second section. This is followed by further examples, and finally by ideas about variants of linear equations and inequalities.


Polite Philosopher Valid Inequality Dine Philosopher Reachable Marking Modulo Equation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  1. 1.Department of Computer ScienceHumboldt-Universität zu BerlinBerlinGermany

Personalised recommendations