In: Rozenberg, G.: Lecture Notes in Computer Science, Vol. 483; Advances in Petri Nets 1990, pages 243-286. Berlin, Germany: Springer-Verlag, 1991.
Abstract: In the analysis part, the authors characterize liveness and boundedness in linear algebraic terms. As a consequence of the new characterizations, both properties are shown to be decidable in polynomial time. They also provide two different kits of sound and complete reduction rules. They address then the problem of synthesizing live and bounded free choice systems within the top-down and the modular design methodologies. The completeness of the kits can be used to prove new results using structural induction. Exact conditions for the preservation of liveness and boundedness under compositions of systems are given. These conditions are the absence of certain design errors.
Keywords: analysis (and) synthesis (of) free choice system(s); liveness decidability; boundedness decidability; linear algebraic term; complete reduction rules; top-down design; modular design; structural induction; liveness preservation; boundedness preservation; design error; killing choices; killing joints; synchronic mismatches; state mismatches.
Back to the Petri Nets Bibliography