Sequential and distributed model checking of Petri nets

Research output: Contribution to journalArticleScientificpeer-review

27 Citations (Scopus)


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 languageEnglish
Pages (from-to)43-60
Number of pages18
JournalInternational journal on software tools for technology transfer
Issue number1
Publication statusPublished - 2005
Externally publishedYes


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


Dive into the research topics of 'Sequential and distributed model checking of Petri nets'. Together they form a unique fingerprint.

Cite this