PV3 ⊧ AdamMCverifies user-specified properties of Petri nets

Application domain/field

• Software-defined networks
• Petri nets (with transits)

Type of tool

Model checker

Expected input

One of the following three options:

1. Software-defined network (up to 82 switches) and a Flow-LTL formula
2. Petri net with transits and a Flow-LTL formula
3. Petri net and a LTL formula

Format:

• Petri nets should be given in PNML (Petri Net Markup Language) or APT format
• It seems to have its own input format to describe the topology of a software-defined network
• (Flow-)LTL formula which should be checked can be passed as a string when calling the model checker

Expected output

SAT or UNSAT If it is UNSAT, then a counterexample is visualized with DOT/Graphviz

Internals

• Model checker for Petri nets with transits against Flow-LTL
• Transit relations are used to follow the flow induced by tokens.
• Flow-LTL is a temporal logic to specify local flow of data and global behavior or markings.
• Note that it can be used to visualize Petri nets with transits (in DOT or pdf file), or a software-defined network (converted to a Petri net with transits, also in DOT or pdf file).
• Uses ABC, MCHyper, Aigertools
• Based on Adam