Document Open Access Logo

Model Checking Strategy-Controlled Rewriting Systems (System Description)

Authors Rubén Rubio , Narciso Martí-Oliet , Isabel Pita , Alberto Verdejo

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2019.34.pdf
  • Filesize: 0.51 MB
  • 18 pages

Document Identifiers

Author Details

Rubén Rubio
  • Facultad de Informática, Universidad Complutense de Madrid, Spain
Narciso Martí-Oliet
  • Facultad de Informática, Universidad Complutense de Madrid, Spain
Isabel Pita
  • Facultad de Informática, Universidad Complutense de Madrid, Spain
Alberto Verdejo
  • Facultad de Informática, Universidad Complutense de Madrid, Spain

Funding

Research partially supported by MCIU Spanish project TRACES (TIN2015-67522-C3-3-R).
  • Rubio, Rubén: Partially supported by MCIU grant FPU17/02319.

Acknowledgements

We are grateful to the reviewers for their careful reading, and their detailed and very useful comments.

Cite As Get BibTex

Rubén Rubio, Narciso Martí-Oliet, Isabel Pita, and Alberto Verdejo. Model Checking Strategy-Controlled Rewriting Systems (System Description). In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 34:1-34:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.FSCD.2019.34

Abstract

Strategies are widespread in Computer Science. In the domain of reduction and rewriting systems, strategies are studied as recipes to restrict and control reduction steps and rule applications, which are intimately local, in a derivation-global sense. This idea has been exploited by various tools and rewriting-based specification languages, where strategies are an additional specification layer. Systems so described need to be analyzed too. This article discusses model checking of systems controlled by strategies and presents a working strategy-aware LTL model checker for the Maude specification language, based on rewriting logic, and its strategy language.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Model checking
  • Theory of computation → Equational logic and rewriting
  • Theory of computation → Rewrite systems
Keywords
  • Model checking
  • strategies
  • Maude
  • rewriting logic

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. Alternating-time temporal logic. Journal of the ACM, 49(5):672-713, 2002. URL: http://dx.doi.org/10.1145/585265.585270.
  2. Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. URL: http://dx.doi.org/10.1017/CBO9781139172752.
  3. Tomás Babiak, Mojmír Kretínský, Vojtech Rehák, and Jan Strejcek. LTL to Büchi automata translation: Fast and more deterministic. In Cormac Flanagan and Barbara König, editors, Tools and Algorithms for the Construction and Analysis of Systems - 18th International Conference, TACAS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings, volume 7214 of LNCS, pages 95-109. Springer, 2012. URL: http://dx.doi.org/10.1007/978-3-642-28756-5_8.
  4. Emilie Balland, Paul Brauner, Radu Kopetz, Pierre-Etienne Moreau, and Antoine Reilles. Tom: Piggybacking Rewriting on Java. In Franz Baader, editor, Term Rewriting and Applications, 18th International Conference, RTA 2007, Paris, France, June 26-28, 2007, Proceedings, volume 4533 of LNCS, pages 36-47. Springer, 2007. URL: http://dx.doi.org/10.1007/978-3-540-73449-9_5.
  5. H.P. Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 131. North Holland, 2nd edition, 2014. Google Scholar
  6. Massimo Bartoletti, Maurizio Murgia, Alceste Scalas, and Roberto Zunino. Modelling and Verifying Contract-Oriented Systems in Maude. In Santiago Escobar, editor, Rewriting Logic and Its Applications - 10th International Workshop, WRLA 2014, Held as a Satellite Event of ETAPS, Grenoble, France, April 5-6, 2014, Revised Selected Papers, volume 8663 of LNCS, pages 130-146. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-319-12904-4_7.
  7. Peter Borovanský, Claude Kirchner, Hélène Kirchner, Pierre-Etienne Moreau, and Christophe Ringeissen. An Overview of ELAN. In Claude Kirchner and Hélène Kirchner, editors, Proceedings of the Second International Workshop on Rewriting Logic and its Applications, WRLA'98, Pont-à-Mousson, France, September 1-4, 1998, volume 15 of ENTCS, pages 55-70. Elsevier, 1998. URL: http://dx.doi.org/10.1016/S1571-0661(05)82552-6.
  8. Tony Bourdier, Horatiu Cirstea, Daniel J. Dougherty, and Hélène Kirchner. Extensional and Intensional Strategies. In Maribel Fernández, editor, Proceedings Ninth International Workshop on Reduction Strategies in Rewriting and Programming, WRS 2009, Brasilia, Brazil, 28th June 2009, volume 15 of EPTCS, pages 1-19, 2009. URL: http://dx.doi.org/10.4204/EPTCS.15.1.
  9. Christiano Braga and Alberto Verdejo. Modular Structural Operational Semantics with Strategies. In Rob van Glabbeek and Peter D. Mosses, editors, Proceedings of the Third Workshop on Structural Operational Semantics, SOS 2006, Bonn, Germany, August 26, 2006, volume 175(1) of ENTCS, pages 3-17. Elsevier, 2007. URL: http://dx.doi.org/10.1016/j.entcs.2006.10.024.
  10. Martin Bravenboer, Karl Trygve Kalleberg, Rob Vermaas, and Eelco Visser. Stratego/XT 0.17. A language and toolset for program transformation. Science of Computer Programming, 72(1-2):52-70, 2008. URL: http://dx.doi.org/10.1016/j.scico.2007.11.003.
  11. Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors. Handbook of Model Checking. Springer, 2018. URL: http://dx.doi.org/10.1007/978-3-319-10575-8.
  12. Manuel Clavel, Francisco Durán, Steven Eker, Santiago Escobar, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, and Carolyn Talcott. Maude Manual v2.7.1, July 2016. URL: http://maude.lcc.uma.es/manual271/maude-manual.html.
  13. Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, and Carolyn L. Talcott. All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic, volume 4350 of LNCS. Springer, 2007. URL: http://dx.doi.org/10.1007/978-3-540-71999-1.
  14. Stefan Edelkamp, Stefan Leue, and Alberto Lluch-Lafuente. Directed explicit-state model checking in the validation of communication protocols. International Journal on Software Tools for Technology Transfer, 5(2-3):247-267, 2004. URL: http://dx.doi.org/10.1007/s10009-002-0104-3.
  15. Steven Eker, Narciso Martí-Oliet, José Meseguer, and Alberto Verdejo. Deduction, Strategies, and Rewriting. In Myla Archer, Thierry Boy de la Tour, and César Muñoz, editors, Proceedings of the 6th International Workshop on Strategies in Automated Deduction, STRATEGIES 2006, Seattle, WA, USA, August 16, 2006, volume 174(11) of ENTCS, pages 3-25. Elsevier, 2007. URL: http://dx.doi.org/10.1016/j.entcs.2006.03.017.
  16. Steven Eker, José Meseguer, and Ambarish Sridharanarayanan. The Maude LTL Model Checker. In Fabio Gadducci and Ugo Montanari, editors, Proceedings of the Fourth International Workshop on Rewriting Logic and its Applications, WRLA 2002, Pisa, Italy, September 19-21, 2002, volume 71 of ENTCS, pages 162-187. Elsevier, 2004. URL: http://dx.doi.org/10.1016/S1571-0661(05)82534-4.
  17. Mercedes Hidalgo-Herrero, Alberto Verdejo, and Yolanda Ortega-Mallén. Using Maude and Its Strategies for Defining a Framework for Analyzing Eden Semantics. In Sergio Antoy, editor, Proceedings of the Sixth International Workshop on Reduction Strategies in Rewriting and Programming, WRS 2006, Seattle, WA, USA, August 11, 2006, volume 174(10) of ENTCS, pages 119-137. Elsevier, 2007. URL: http://dx.doi.org/10.1016/j.entcs.2007.02.051.
  18. C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985. Google Scholar
  19. Hélène Kirchner. Rewriting Strategies and Strategic Rewrite Programs. In Narciso Martí-Oliet, Peter Csaba Ölveczky, and Carolyn L. Talcott, editors, Logic, Rewriting, and Concurrency - Essays dedicated to José Meseguer on the Occasion of His 65th Birthday, volume 9200 of LNCS, pages 380-403. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-319-23165-5_18.
  20. Saul Kripke. A Completeness Theorem in Modal Logic. Journal of Symbolic Logic, 24(1):1-14, 1959. URL: http://dx.doi.org/10.2307/2964568.
  21. Orna Kupferman and Moshe Y. Vardi. Memoryful Branching-Time Logic. In 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12-15 August 2006, Seattle, WA, USA, Proceedings, pages 265-274. IEEE Computer Society, 2006. URL: http://dx.doi.org/10.1109/LICS.2006.34.
  22. Weiwei Li, Shuanglong Kan, and Zhiqiu Huang. A Better Translation From LTL to Transition-Based Generalized Büchi Automata. IEEE Access, 5:27081-27090, 2017. URL: http://dx.doi.org/10.1109/ACCESS.2017.2773123.
  23. Si Liu, Muntasir Raihan Rahman, Stephen Skeirik, Indranil Gupta, and José Meseguer. Formal Modeling and Analysis of Cassandra in Maude. In Stephan Merz and Jun Pang, editors, Formal Methods and Software Engineering - 16th International Conference on Formal Engineering Methods, ICFEM 2014, Luxembourg, Luxembourg, November 3-5, 2014. Proceedings, volume 8829 of LNCS, pages 332-347. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-319-11737-9_22.
  24. Narciso Martí-Oliet, Miguel Palomino, and Alberto Verdejo. Strategies and simulations in a semantic framework. Journal of Algorithms, 62(3-4):95-116, 2007. URL: http://dx.doi.org/10.1016/j.jalgor.2007.04.002.
  25. Narciso Martí-Oliet, José Meseguer, and Alberto Verdejo. Towards a Strategy Language for Maude. In Narciso Martí-Oliet, editor, Proceedings of the Fifth International Workshop on Rewriting Logic and its Applications, WRLA 2004, Barcelona, Spain, March 27-April 4, 2004, volume 117 of ENTCS, pages 417-441. Elsevier, 2004. URL: http://dx.doi.org/10.1016/j.entcs.2004.06.020.
  26. José Meseguer. Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science, 96(1):73-155, 1992. URL: http://dx.doi.org/10.1016/0304-3975(92)90182-F.
  27. Fabio Mogavero, Aniello Murano, Giuseppe Perelli, and Moshe Y. Vardi. Reasoning About Strategies: On the Model-Checking Problem. ACM Transactions in Computational Logic, 15(4):34:1-34:47, 2014. URL: http://dx.doi.org/10.1145/2631917.
  28. Martin R. Neuhäußer and Thomas Noll. Abstraction and Model Checking of Core Erlang Programs in Maude. In Grit Denker and Carolyn Talcott, editors, Proceedings of the 6th International Workshop on Rewriting Logic and its Applications, WRLA 2006, Vienna, Austria, April 1-2, 2006, volume 176 (4) of ENTCS, pages 147-163. Elsevier, 2007. URL: http://dx.doi.org/10.1016/j.entcs.2007.06.013.
  29. Amir Pnueli. The Temporal Logic of Programs. In 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977, pages 46-57. IEEE Computer Society, 1977. URL: http://dx.doi.org/10.1109/SFCS.1977.32.
  30. Rubén Rubio, Narciso Martí-Oliet, Isabel Pita, and Alberto Verdejo. Model checking strategy-controlled rewriting systems (extended version). Technical Report 02/19, Departamento de Sistemas Informáticos y Computación, Universidad Complutense de Madrid, 2019. URL: http://maude.sip.ucm.es/strategies/tr0219.pdf.
  31. Gustavo Santos-García and Miguel Palomino. Solving Sudoku Puzzles with Rewriting Rules. In Grit Denker and Carolyn Talcott, editors, Proceedings of the 6th International Workshop on Rewriting Logic and its Applications, WRLA 2006, Vienna, Austria, April 1-2, 2006, volume 176 (4) of ENTCS, pages 79-93. Elsevier, 2007. URL: http://dx.doi.org/10.1016/j.entcs.2007.06.009.
  32. Terese. Term Rewriting Systems. Cambridge University Press, 2003. Google Scholar
  33. Alberto Verdejo and Narciso Martí-Oliet. Basic completion strategies as another application of the Maude strategy language. In Santiago Escobar, editor, Proceedings 10th International Workshop on Reduction Strategies in Rewriting and Programming, WRS 2011, Novi Sad, Serbia, 29 May 2011, volume 82 of EPTCS, pages 17-36, 2011. URL: http://dx.doi.org/10.4204/EPTCS.82.2.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact