MC-SOG: An LTL Model Checker Based on Symbolic Observation Graphs

mc-sog allows to check LTL formulae on ordinary bounded Petri nets by the exploration of the corresponding Symbolic Observation Graph [1]. Its implementation is based on the object-oriented model checking library Spot and the binary decision diagram Buddy.

The tool requires:

• The maximal number of tokens which can be stored in any place (to determine how many binary variables are needed to encode a marking). 
• An LTL formula respecting the syntax defined by the LTL parser of Spot..

The atomic propositions are simply the names of the Petri net places. In a given reachable marking, a proposition is satisfied if the corresponding place contains at least one token.

The tool only indicates if the net satisfies or not the formula, i.e. no counter example is given. In a close future, the computation of counter examples will be integrated.

Reference

[1]  MC-SOG: An LTL Model Checker Based on Symbolic Observation Graphs, Kais Klai and Denis Poitrenaud, 29th International Conference on Application and Theory of Petri Nets (ICATPN'08), Springer, LNCS vol. 5062, pp 288-306, Xi'an, China, June 2008.