Abstract
Maude 3 includes as a new feature an object-level strategy language. Rewriting strategies can now be used to easily control how rules are applied, restricting the rewriting systems behavior. This new specification layer would not be useful if there were no tools to execute, analyze and verify its creatures. For that reason, we extended the Maude LTL model checker to systems controlled by strategies, after studying their model-checking problem. Now, we widen the range of properties that can be checked in Maude models, both strategy-aware and strategy-free, by implementing a module for the language-independent model checker LTSmin that supports logics like CTL* and \(\mu \)-calculus.
Research partially supported by MCI Spanish project TRACES (TIN2015-67522-C3-3-R). Rubén Rubio is partially supported by MU grant FPU17/02319.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
A rewrite theory is coherent if for any term t rewritten by a rule to a term \(t'\), its canonical form u modulo equations and axioms can be rewritten to a term \(u'\) that is equationally equivalent to \(t'\), see [13, §5.3]. Coherence is assumed by Maude, which reduces terms to their canonical forms before applying a rule, not to miss any rewrite.
- 2.
For simplicity, we are obviating finite and failed executions. More precisely, \(\mathcal {M}\) should only include states Q from which a solution or an infinite execution can be reached.
- 3.
LTSmin uses the dlopen API to load libmaudemc.so into memory, and then the function dlsym to obtain pointers to its symbols (global variables, functions..., namely those required by the PINS interface) so that they can be read and called.
- 4.
It could be necessary to execute one or more rewrites until realizing that an execution path should be abandoned (by an explicit fail, a failed test...) These are implicitly ignored by the nested depth-first search of the LTL algorithm, since no cycles can be found through them, but they must be explicitly purged for other algorithms.
- 5.
Our syntax for \(\mu \)-calculus lets modalities take a list of rule labels, where \(\langle C \rangle \, \varphi = \bigvee _{a \in C} \langle a \rangle \, \varphi \), which can be preceded by a negation symbol
to indicate its complement.
References
Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49(5), 672–713 (2002). https://doi.org/10.1145/585265.585270
Amparore, E., et al.: Presentation of the 9th edition of the model checking contest. In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.) TACAS 2019. LNCS, vol. 11429, pp. 50–68. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17502-3_4
Bae, K., Escobar, S., Meseguer, J.: Abstract logical model checking of infinite-state systems using narrowing. In: van Raamsdonk, F. (ed.) 24th International Conference on Rewriting Techniques and Applications, RTA 2013, June 24–26, 2013, Eindhoven, The Netherlands. LIPIcs, vol. 21, pp. 81–96. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2013). https://doi.org/10.4230/LIPIcs.RTA.2013.81
Bae, K., Meseguer, J.: Model checking linear temporal logic of rewriting formulas under localized fairness. Sci. Comput. Program. 99, 193–234 (2015). https://doi.org/10.1016/j.scico.2014.02.006
Billington, J., et al.: PNML reference site. http://www.pnml.org/
Borovanský, P., Kirchner, C., Kirchner, H., Ringeissen, C.: Rewriting with strategies in ELAN: a functional semantics. Int. J. Found. Comput. Sci. 12(1), 69–95 (2001). https://doi.org/10.1142/S0129054101000412
Bourdier, T., Cirstea, H., Dougherty, D.J., Kirchner, H.: Extensional and intensional strategies. In: Fernández, M. (ed.) Proceedings Ninth International Workshop on Reduction Strategies in Rewriting and Programming, WRS 2009, Brasilia, Brazil, 28th June 2009. EPTCS, vol. 15, pp. 1–19 (2009). https://doi.org/10.4204/EPTCS.15.1
Bravenboer, M., Kalleberg, K.T., Vermaas, R., Visser, E.: Stratego/XT 0.17. A language and toolset for program transformation. Sci. Comput. Program. 72(1–2), 52–70 (2008). https://doi.org/10.1016/j.scico.2007.11.003
Casagrande, A.: pyModelChecking. A simple Python model-checking package. https://pypi.org/project/pyModelChecking/
Cimatti, A.A., et al.: NuSMV 2: an OpenSource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45657-0_29
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)
Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.): Handbook of Model Checking. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-10575-8
Clavel, M., et al.: Maude Manual v3.1 (2020–10). http://maude.lcc.uma.es/maude31-manual-html/maude-manual.html
Clavel, M., Meseguer, J.: Reflection and strategies in rewriting logic. In: Meseguer, J. (ed.) Proceedings of the First International Workshop on Rewriting Logic and its Applications, WRLA 1996, Asilomar, California, 3–6 September 1996. Electronic Notes in Theoretical Computer Science, vol. 4, pp. 126–148. Elsevier (1996). https://doi.org/10.1016/S1571-0661(04)00037-4
Clavel, M., Meseguer, J.: Internal strategies in a reflective logic. In: Gramlich, B., Kirchner, H. (eds.) Proceedings of the CADE 2014 Workshop on Strategies in Automated Deduction, pp. 1–12 (1997)
Durán, F., et al.: Programming and symbolic computation in Maude. J. Log. Algebr. Methods Comput. Program. 110, 1–58 (2020). https://doi.org/10.1016/j.jlamp.2019.100497
Eker, S., Martí-Oliet, N., Meseguer, J., Verdejo, A.: Deduction, strategies, and rewriting. In: Archer, M., de la Tour, T.B., Muñoz, C. (eds.) Proceedings of the 6th International Workshop on Strategies in Automated Deduction, STRATEGIES 2006, Seattle, WA, USA, 16 August 2006. Electronic Notes in Theoretical Computer Science, vol. 174(11), pp. 3–25. Elsevier (2007). https://doi.org/10.1016/j.entcs.2006.03.017
Eker, S., Martí-Oliet, N., Meseguer, J., Pita, I., Rubio, R., Verdejo, A.: Strategy language for Maude. http://maude.ucm.es/strategies
Eker, S., Meseguer, J., Sridharanarayanan, A.: The Maude LTL model checker. In: Gadducci, F., Montanari, U. (eds.) Proceedings of the Fourth International Workshop on Rewriting Logic and its Applications, WRLA 2002, Pisa, Italy, 19–21 September 2002. Electronic Notes in Theoretical Computer Science, vol. 71, pp. 162–187. Elsevier (2004). https://doi.org/10.1016/S1571-0661(05)82534-4
FADoSS: Experimental language bindings for Maude. https://github.com/fadoss/maude-bindings
Gastin, P., Oddoux, D.: Fast LTL to Büchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 53–65. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-44585-4_6
Holzmann, G., et al.: Spin - Formal verification. https://spinroot.com
Kant, G., Laarman, A., Meijer, J., van de Pol, J., Blom, S., van Dijk, T.: LTSmin: high-performance language-independent model checking. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 692–707. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0_61
Kupferman, O., Vardi, M.Y.: Memoryful branching-time logic. In: Alur, R. (ed.) 21th IEEE Symposium on Logic in Computer Science (LICS 2006), Seattle, WA, USA, 12–15 August 2006. Proceedings, pp. 265–274. IEEE Computer Society (2006). https://doi.org/10.1109/LICS.2006.34
Larsen, K.G., et al.: UPPAAL. http://www.uppaal.org/
Lepri, D., Ábrahám, E., Ölveczky, P.C.: Sound and complete timed CTL model checking of timed Kripke structures and real-time rewrite theories. Sci. Comput. Program. 99, 128–192 (2015). https://doi.org/10.1016/j.scico.2014.06.006
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, 27 March–4 April 2004. Electronic Notes in Theoretical Computer Science, vol. 117, pp. 417–441. Elsevier (2004). https://doi.org/10.1016/j.entcs.2004.06.020
Martí-Oliet, N., Palomino, M., Verdejo, A.: Strategies and simulations in a semantic framework. J. Algorithms 62(3–4), 95–116 (2007). https://doi.org/10.1016/j.jalgor.2007.04.002
Mogavero, F., Murano, A., Perelli, G., Vardi, M.Y.: Reasoning about strategies: on the model-checking problem. ACM Trans. Comput. Log. 15(4), 34:1–34:47 (2014). https://doi.org/10.1145/2631917
Palomino, M., Martí-Oliet, N., Verdejo, A.: Playing with Maude. In: Abdennadher, S., Ringeissen, C. (eds.) Proceedings of the 5th International Workshop on Rule-Based Programming, RULE 2004, Aachen, Germany, 1 June 2004. Electronic Notes in Theoretical Computer Science, vol. 124(1), pp. 3–23. Elsevier (2005). https://doi.org/10.1016/j.entcs.2004.07.012
Ročkai, P., Barnat, J., Štill, V., et al.: DIVINE. https://divine.fi.muni.cz/
Rubio, R., Martí-Oliet, N., Pita, I., Verdejo, A.: Model checking strategy-controlled rewriting systems. In: Geuvers, H. (ed.) 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, 24–30 June 2019, Dortmund, Germany. LIPIcs, vol. 131, pp. 34:1–34:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019). https://doi.org/10.4230/LIPIcs.FSCD.2019.31
Rubio, R., Martí-Oliet, N., Pita, I., Verdejo, A.: Parameterized strategies specification in Maude. In: Fiadeiro, J.L., Ţuţu, I.I., et al. (eds.) WADT 2018. LNCS, vol. 11563, pp. 27–44. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-23220-7_2
Santos-Buitrago, B., Riesco, A., Knapp, M., Alcantud, J.C.R., Santos-García, G., Talcott, C.L.: Soft set theory for decision making in computational biology under incomplete information. IEEE Access 7, 18183–18193 (2019). https://doi.org/10.1109/ACCESS.2019.2896947
Santos-García, G., Palomino, M.: Solving Sudoku puzzles with rewriting rules. In: Denker, G., Talcott, C. (eds.) Proceedings of the 6th International Workshop on Rewriting Logic and its Applications, WRLA 2006, Vienna, Austria, 1–2 April 2006. Electronic Notes in Theoretical Computer Science, vol. 176(4), pp. 79–93. Elsevier (2007). https://doi.org/10.1016/j.entcs.2007.06.009
Thomas, W.: Computation tree logic and regular \(\upomega \)-languages. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) REX 1988. LNCS, vol. 354, pp. 690–713. Springer, Heidelberg (1989). https://doi.org/10.1007/BFb0013041
Verdejo, A., Martí-Oliet, N.: Basic completion strategies as another application of the Maude strategy language. In: Escobar, S. (ed.) Proceedings 10th International Workshop on Reduction Strategies in Rewriting and Programming, WRS 2011, Novi Sad, Serbia, 29 May 2011. EPTCS, vol. 82, pp. 17–36 (2011). https://doi.org/10.4204/EPTCS.82.2
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
Cite this paper
Rubio, R., Martí-Oliet, N., Pita, I., Verdejo, A. (2020). Strategies, Model Checking and Branching-Time Properties in Maude. In: Escobar, S., Martí-Oliet, N. (eds) Rewriting Logic and Its Applications. WRLA 2020. Lecture Notes in Computer Science(), vol 12328. Springer, Cham. https://doi.org/10.1007/978-3-030-63595-4_9
Download citation
DOI: https://doi.org/10.1007/978-3-030-63595-4_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-63594-7
Online ISBN: 978-3-030-63595-4
eBook Packages: Computer ScienceComputer Science (R0)