@inproceedings{
    Vrp94c,
    editor = {Desel, J{\"{o}}rg and Oberweis, Andreas and Reisig, Wolfgang},
    author = "Varpaaniemi, Kimmo",
    publisher = {Forschungsberichte, Bericht 309, Institut f{\"{u}}r Angewandte Informatik und Formale Beschreibungsverfahren, Universit{\"{a}}t Karlsruhe (TH), Germany},
    title = "{O}n-the-Fly Verification with {P}{R}{O}{D}",
    booktitle = {{A}lgorithmen und {W}erkzeuge f{\"{u}}r {P}etrinetze: {W}orkshop der {G}{I}-{F}achgruppe 0.0.1, ``{P}etrinetze und verwandte {S}ystemmodelle'', {B}erlin, 10.--11. {O}ktober 1994},
    ps = "kvawpn94.ps",
    pages = "80--83",
    flags = "public",
    year = "1994",
    keywords = "predicate/transition nets, reachability analysis, on-the-fly verification, linear time temporal properties, stubborn set method",
    pdf = "kvawpn94.pdf",
    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. \par 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. \par In this paper we describe how the Pr/T-net reachability analysis tool PROD verifies properties on-the-fly."
}