DROPS

Document

System Description

DOI: 10.4230/LIPIcs.FSCD.2019.34

Model Checking Strategy-Controlled Rewriting Systems (System Description)

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

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)

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.

Cite as

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)

Copy BibTex To Clipboard

@InProceedings{rubio_et_al:LIPIcs.FSCD.2019.34,
  author =	{Rubio, Rub\'{e}n and Mart{\'\i}-Oliet, Narciso and Pita, Isabel and Verdejo, Alberto},
  title =	{{Model Checking Strategy-Controlled Rewriting Systems}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{34:1--34:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Geuvers, Herman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.34},
  URN =		{urn:nbn:de:0030-drops-105414},
  doi =		{10.4230/LIPIcs.FSCD.2019.34},
  annote =	{Keywords: Model checking, strategies, Maude, rewriting logic}
}

Document

DOI: 10.4230/LIPIcs.RTA.2010.277

Declarative Debugging of Missing Answers for Maude

Authors: Adrian Riesco, Alberto Verdejo, and Narciso Marti-Oliet

Published in: LIPIcs, Volume 6, Proceedings of the 21st International Conference on Rewriting Techniques and Applications (2010)

Abstract

Declarative debugging is a semi-automatic technique that starts from an incorrect computation and locates a program fragment responsible for the error by building a tree representing this computation and guiding the user through it to find the error. Membership equational logic (MEL) is an equational logic that in addition to equations allows the statement of membership axioms characterizing the elements of a sort. Rewriting logic is a logic of change that extends MEL by adding rewrite rules, that correspond to transitions between states and can be nondeterministic. In this paper we propose a calculus that allows to infer normal forms and least sorts with the equational part, and sets of reachable terms through rules. We use an abbreviation of the proof trees computed with this calculus to build appropriate debugging trees for missing answers (results that are erroneous because they are incomplete), whose adequacy for debugging is proved. Using these trees we have implemented a declarative debugger for Maude, a high-performance system based on rewriting logic, whose use is illustrated with an example.

Cite as

Adrian Riesco, Alberto Verdejo, and Narciso Marti-Oliet. Declarative Debugging of Missing Answers for Maude. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics (LIPIcs), Volume 6, pp. 277-294, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{riesco_et_al:LIPIcs.RTA.2010.277,
  author =	{Riesco, Adrian and Verdejo, Alberto and Marti-Oliet, Narciso},
  title =	{{Declarative Debugging of Missing Answers for Maude}},
  booktitle =	{Proceedings of the 21st International Conference on Rewriting Techniques and Applications},
  pages =	{277--294},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-18-7},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{6},
  editor =	{Lynch, Christopher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2010.277},
  URN =		{urn:nbn:de:0030-drops-26589},
  doi =		{10.4230/LIPIcs.RTA.2010.277},
  annote =	{Keywords: Declarative debugging, Maude, Missing answers, Rewriting}
}

Search Results

Documents authored by Verdejo, Alberto

Model Checking Strategy-Controlled Rewriting Systems (System Description)

Abstract

Cite as

Declarative Debugging of Missing Answers for Maude

Abstract

Cite as

Thanks for your feedback!

Could not send message