PV3 ⊧ AdamMCverifies user-specified properties of Petri nets
- Software-defined networks
- Petri nets (with transits)
Type of toolModel checker
Expected inputOne of the following three options:
- Software-defined network (up to 82 switches) and a Flow-LTL formula
- Petri net with transits and a Flow-LTL formula
- Petri net and a LTL formula
- 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 outputSAT or UNSAT If it is UNSAT, then a counterexample is visualized with DOT/Graphviz
- 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