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.
KeywordsPolite Philosopher Valid Inequality Dine Philosopher Reachable Marking Modulo Equation
Unable to display preview. Download preview PDF.