In: J. Desel, A. Oberweis & W. Reisig (Eds.), Algorithmen und Werkzeuge für Petrinetze:Workshop der GI-Fachgruppe 0.0.1,``Petrinetze und verwandte Systemmodelle'',Berlin, 10.-11. Oktober 1994, Universität Karlsruhe (TH), Institut für Angewandte Informatik und Formale Beschreibungsverfahren, Forschungsberichte, Bericht 309, pages 80-83. October 1994.
Abstract: On-the-fly verification of a property means that the property is verified during state space generation, in contrary to the traditional approach where properties are verified after state space generation. As soon as it is known whether the property holds, the generation of the state space can be stopped. Since an erroneous system can have a much larger state space than the intended correct system, it is important to find errors as soon as possible. On the other hand, even in the case that all states become generated, the overhead caused by on-the-fly verification, compared to non-on-the-fly verification, is often negligible.
It has turned out that many of the methods that have originally been designed to avoid the generation of all states in non-on-the fly verification can be applied to on-the-fly verification as well. Valmari's stubborn set method is one such method.
In this paper we describe how the Pr/T-net reachability analysis tool PROD verifies properties on-the-fly.
Keywords: predicate/transition nets; reachability analysis; on-the-fly verification; linear time temporal properties; stubborn set method.