Model Checking TLR* Guarantee Formulas on Infinite Systems

  • Óscar Martín
  • Alberto Verdejo
  • Narciso Martí-Oliet
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8373)


We present the implementation of a model checker for systems with a potentially infinite number of reachable states. It has been developed in the rewriting-logic language Maude. The model checker is explicit-state, that is, not symbolic. In infinite systems, we cannot expect it to finish in every case: it provides a semi-decision algorithm to validate guarantee formulas (or, equivalently, to falsify safety ones). To avoid getting lost in infinite paths, search is always performed within bounded depth. The properties to be checked are written in the Temporal Logic of Rewriting, TLR*, a generalization of CTL* that uses atomic propositions both on states and on transitions, providing, in this way, a richer expressive power. As an intermediate step, a strategy language is used. Guarantee formulas are first translated into strategy expressions and, then, the system and the strategy evolve in parallel searching for computations that satisfy the strategy and, thus, the formula. An example on verifying cache coherence protocols is presented, showing the usefulness of the tool.


Infinite-state system rewriting logic Maude model checking strategy temporal logic TLR* guarantee formula cache coherence 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite-state systems. In: LICS, pp. 313–321. IEEE Computer Society Press (1996)Google Scholar
  2. 2.
    Bae, K., Escobar, S., Meseguer, J.: Abstract logical model checking of infinite-state systems using narrowing. In: van Raamsdonk, F. (ed.) RTA. LIPIcs, vol. 21, pp. 81–96. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2013)Google Scholar
  3. 3.
    Bae, K., Meseguer, J.: The linear temporal logic of rewriting Maude model checker. In: Ölveczky, P.C. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 208–225. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  4. 4.
    Bae, K., Meseguer, J.: State/event-based LTL model checking under parametric generalized fairness. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 132–148. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  5. 5.
    Bae, K., Meseguer, J.: Model checking LTLR formulas under localized fairness. In: Durán, F. (ed.) WRLA 2012. LNCS, vol. 7571, pp. 99–117. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  6. 6.
    Bae, K., Meseguer, J.: A rewriting-based model checker for the linear temporal logic of rewriting. Electr. Notes Theor. Comput. Sci. 290, 19–36 (2012)CrossRefzbMATHGoogle Scholar
  7. 7.
    Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Advances in Computers 58, 117–148 (2003)CrossRefGoogle Scholar
  8. 8.
    Borovanský, P., Kirchner, C., Kirchner, H., Moreau, P.-E.: ELAN from a rewriting logic point of view. Theoretical Computer Science 285(2), 155–185 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Bruni, R., Meseguer, J.: Semantic foundations for generalized rewrite theories. Theoretical Computer Science 360(1-3), 386–414 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    Clarke, E.M., Grumberg, O., Peled, D.: Model checking. MIT Press (2001)Google Scholar
  11. 11.
    Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.L.: All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic. LNCS, vol. 4350. Springer, Heidelberg (2007)Google Scholar
  12. 12.
    De Nicola, R., Vaandrager, F.W.: Action versus state based logics for transition systems. In: Guessarian, I. (ed.) Semantics of Systems of Concurrent Processes. LNCS, vol. 469, pp. 407–419. Springer, Heidelberg (1990)CrossRefGoogle Scholar
  13. 13.
    Escobar, S., Meseguer, J.: Symbolic model checking of infinite-state systems using narrowing. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 153–168. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  14. 14.
    Farzan, A.: Static and Dynamic Formal Analysis of Concurrent Systems and Languages: A Semantics-Based Approach. PhD thesis, Department of Computer Science, University of Illinois at Urbana-Champaign (2007)Google Scholar
  15. 15.
    Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theor. Comput. Sci. 256(1-2), 63–92 (2001)MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. Journal of the ACM 32(1), 137–161 (1985)MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Martí-Oliet, N., Meseguer, J., Verdejo, A.: Towards a strategy language for Maude. In: Martí-Oliet, N. (ed.) Proceedings of the Fifth International Workshop on Rewriting Logic and its Applications, WRLA 2004, Barcelona, Spain, March 27-April 4. Electronic Notes in Theoretical Computer Science, vol. 117, pp. 417–441. Elsevier (2004)Google Scholar
  18. 18.
    Martín, Ó.: Model checking TLR* guarantee formulas on infinite systems. Master’s thesis, Facultad de Informática, Universidad Complutense de Madrid (July 2013),
  19. 19.
    Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96(1), 73–155 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  20. 20.
    Meseguer, J.: The temporal logic of rewriting. Technical Report UIUCDCS-R-2007-2815, Department of Computer Science, University of Illinois at Urbana-Champaign (2007)Google Scholar
  21. 21.
    Meseguer, J., Palomino, M., Martí-Oliet, N.: Equational abstractions. Theoretical Computer Science 403(2-3), 239–264 (2008)MathSciNetCrossRefzbMATHGoogle Scholar
  22. 22.
    Visser, E.: A survey of strategies in program transformation systems. Electr. Notes Theor. Comput. Sci. 57, 109–143 (2001)CrossRefzbMATHGoogle Scholar
  23. 23.
    VMware. vSphere Virtual Machine Administration (update 1, ESXi 5.1, vCenter Server 5.1),

Copyright information

© Springer-Verlag Berlin Heidelberg 2014

Authors and Affiliations

  • Óscar Martín
    • 1
  • Alberto Verdejo
    • 1
  • Narciso Martí-Oliet
    • 1
  1. 1.Facultad de InformáticaUniversidad Complutense de MadridSpain

Personalised recommendations