Sequential and distributed model checking of Petri nets

A. Bell, Boudewijn R.H.M. Haverkort

    Research output: Contribution to journalArticleAcademicpeer-review

    27 Citations (Scopus)
    50 Downloads (Pure)


    In this paper we present sequential as well as distributed algorithms for model checking computational tree logic over finite-state systems specified as Petri nets. The algorithms rely on an explicit representation of the systemrsquos state space but do not require the transition relation to be explicitly available; it is recomputed whenever required. This approach allows us to model check very large systems, with hundreds of millions of states, in a fast and efficient way. For the case studies addressed, the distributed algorithms scale very well, as they show efficiencies in the range of 60% to 95%, depending on the test cases and case studies at hand.
    Original languageUndefined
    Article number10.1007/s10009-003-0129-2
    Pages (from-to)43-60
    Number of pages18
    JournalInternational journal on software tools for technology transfer
    Issue number1
    Publication statusPublished - 2005


    • EWI-7871
    • IR-63632
    • METIS-224117

    Cite this