From PNML to counter systems for accelerating Petri Nets with FAST

Sébastien Bardin (1) , Laure Petrucci (2)

1 SECSI - Security of information systems
2 LIPN - Laboratoire d'Informatique de Paris-Nord

We use the tool FAST to check parameterized safety properties on Petri nets with a large or infinite state space. Although this tool is not dedicated to Petri nets, it can be used for these as place/transition nets (and some of their extensions) are subcases of FASTinput model. The originality of the tool lies in the use of acceleration techniques in order to compute the exact reachability set for infinite systems. In this paper, we present the automatic transformation of Petri nets written in PNML (Petri Net Markup Language) into counter systems. Then, FAST provides a simple but very powerful language to express complex properties and check these.

Domaines: Autre [cs.OH]

Sébastien Bardin, Laure Petrucci. From PNML to counter systems for accelerating Petri Nets with FAST. Workshop on Interchange Formats for Petri Nets, 2004, Bologna, Italy. pp.26-40. ⟨hal-00003391⟩