A Completion of the S-invariance Technique by means of Fixed Point Algorithms
Kurt Lautenbach, H. N. de Ridder, Koblenz-Landau Univ., Koblenz (Germany). Inst. fuer Informatik · 1995
: In this paper we transform bounded Petri net systems into transition systems in order to have a bridge between Petri nets and temporal logic. We then use structural knowledge of the Petri nets (S--invariants, traps) to accelerate fixed point calculations in the transition systems. This technique comprises solutions of such problems which are not solvable by S--invariance technique. By a new concept for a very compact representation of net markings, the ordered natural decision diagrams (ONDDs), we gain a further considerable acceleration of the fixed point calculations. The ONDDs are a generalization of the ordered binary decision diagrams (OBDDs) due to Bryant. Keywords: Petri nets, S--invariants, traps, transition systems, temporal logic, ordered natural decision diagrams (ONDDs), ordered binary decision diagrams (OBDDs) Table of Contents 1 Introduction : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 3 2 Transition Systems and Fixed Point Operators : : : : : : : ...