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

  • Kais Klai
  • Denis Poitrenaud
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5062)


Model checking is a powerful and widespread technique for the verification of finite distributed systems. However, the main hindrance for wider application of this technique is the well-known state explosion problem. During the last two decades, numerous techniques have been proposed to cope with the state explosion problem in order to get a manageable state space. Among them, on-the-fly model-checking allows for generating only the ”interesting” part of the model while symbolic model-checking aims at checking the property on a compact representation of the system by using Binary Decision Diagram (BDD) techniques. In this paper, we propose a technique which combines these two approaches to check LTL∖X state-based properties over finite systems. During the model checking process, only an abstraction of the state space of the system, namely the symbolic observation graph, is (possibly partially) explored. The building of such an abstraction is guided by the property to be checked and is equivalent to the original state space graph of the system w.r.t. LTL∖X logic (i.e. the abstraction satisfies a given formula ϕ iff the system satisfies ϕ). Our technique was implemented for systems modeled by Petri nets and compared to an explicit model-checker as well as to a symbolic one (NuSMV) and the obtained results are very competitive.


Model Checker Linear Temporal Logic Atomic Proposition Binary Decision Diagram Kripke Structure 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Bryant, R.E.: Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys 24(3), 293–318 (1992)CrossRefGoogle Scholar
  2. 2.
    Ciardo, G., Lüttgen, G., Siminiceanu, R.: Efficient symbolic state-space construction for asynchronous systems. In: Nielsen, M., Simpson, D. (eds.) ICATPN 2000. LNCS, vol. 1825, pp. 103–122. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  3. 3.
    Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NUSMV: A new symbolic model checker. International Journal on Software Tools for Technology Transfer 2(4), 410–425 (2000)zbMATHCrossRefGoogle Scholar
  4. 4.
    Clarke, E.M., Grumberg, O., Hamaguchi, K.: Another look at LTL model checking. Formal Methods in System Design 10(1), 47–71 (1997)CrossRefGoogle Scholar
  5. 5.
    Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (2000)Google Scholar
  6. 6.
    Clarke, E.M., McMillan, K.L., Campos, S.V.A., Hartonas-Garmhausen, V.: Symbolic model checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 419–427. Springer, Heidelberg (1996)Google Scholar
  7. 7.
    Cleaveland, R., Hennessy, M.: Testing equivalence as a bisimulation equivalence. In: Proceedings of the international workshop on Automatic verification methods for finite state systems, pp. 11–23. Springer, New York (1990)Google Scholar
  8. 8.
    Couvreur, J.-M.: On-the-fly verification of linear temporal logic. In: Woodcock, J.C.P., Davies, J., Wing, J.M. (eds.) FM 1999. LNCS, vol. 1709, pp. 253–271. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  9. 9.
    Duret-Lutz, A., Poitrenaud, D.: SPOT: an extensible model checking library using transition-based generalized Büchi automata. In: Proceedings of the 12th IEEE/ACM International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems (MASCOTS 2004), Volendam, The Netherlands, pp. 76–83. IEEE Computer Society Press, Los Alamitos (2004)CrossRefGoogle Scholar
  10. 10.
    Geldenhuys, J., Valmari, A.: Techniques for smaller intermediary BDDs. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 233–247. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  11. 11.
    Goltz, U., Kuiper, R., Penczek, W.: Propositional temporal logics and equivalences. In: CONCUR, pp. 222–236 (1992)Google Scholar
  12. 12.
    Haddad, S., Ilié, J.-M., Klai, K.: Design and evaluation of a symbolic and abstraction-based model checker. In: Wang, F. (ed.) ATVA 2004. LNCS, vol. 3299, pp. 196–210. Springer, Heidelberg (2004)Google Scholar
  13. 13.
    Henzinger, T.A., Kupferman, O., Vardi, M.Y.: A space-efficient on-the-fly algorithm for real-time model checking. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 514–529. Springer, Heidelberg (1996)Google Scholar
  14. 14.
    Kaivola, R., Valmari, A.: The weakest compositional semantic equivalence preserving nexttime-less linear temporal logic. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol. 630, pp. 207–221. Springer, Heidelberg (1992)CrossRefGoogle Scholar
  15. 15.
    Manna, Z., Pnueli, A.: The temporal logic of reactive and concurrent systems. Springer, New York (1992)Google Scholar
  16. 16.
    Pastor, E., Roig, O., Cortadella, J., Badia, R.: Petri net analysis using boolean manipulation. In: Valette, R. (ed.) ICATPN 1994. LNCS, vol. 815, pp. 416–435. Springer, Heidelberg (1994)Google Scholar
  17. 17.
    Peterson, J.L.: Petri Net Theory and the Modeling of Systems. Prentice Hall PTR, Upper Saddle River, NJ, USA (1981)Google Scholar
  18. 18.
    Puhakka, A., Valmari, A.: Weakest-congruence results for livelock-preserving equivalences. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 510–524. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  19. 19.
    Rozier, K., Vardi, M.: LTL satisfiability checking. In: Bošnački, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 149–167. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  20. 20.
    Tao, Z.P., von Bochmann, G., Dssouli, R.: Verification and diagnosis of testing equivalence and reduction relation. In: ICNP 1995: Proceedings of the 1995 International Conference on Network Protocols, Washington, DC, USA, p. 14. IEEE Computer Society, Los Alamitos (1995)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Kais Klai
    • 1
  • Denis Poitrenaud
    • 2
  1. 1.LIPN, CNRS UMR 7030Université Paris 13VilletaneuseFrance
  2. 2.LIP6, CNRS UMR 7606Université P. et M. CurieParisFrance

Personalised recommendations