DROPS

Document

DOI: 10.4230/LIPIcs.CONCUR.2024.24

Validity of Contextual Formulas

Authors: Javier Esparza and Rubén Rubio

Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)

Abstract

Many well-known logical identities are naturally written as equivalences between contextual formulas. A simple example is the Boole-Shannon expansion c[p] ≡ (p ∧ c[true]) ∨ (¬ p ∧ c[false]), where c denotes an arbitrary formula with possibly multiple occurrences of a "hole", called a context, and c[φ] denotes the result of "filling" all holes of c with the formula φ. Another example is the unfolding rule μX.c[X] ≡ c[μX.c[X]] of the modal μ-calculus. We consider the modal μ-calculus as overarching temporal logic and, as usual, reduce the problem whether φ₁ ≡ φ₂ holds for contextual formulas φ₁, φ₂ to the problem whether φ₁ ↔ φ₂ is valid. We show that the problem whether a contextual formula of the μ-calculus is valid for all contexts can be reduced to validity of ordinary formulas. Our first result constructs a canonical context such that a formula is valid for all contexts iff it is valid for this particular one. However, the ordinary formula is exponential in the nesting-depth of the context variables. In a second result we solve this problem, thus proving that validity of contextual formulas is EXP-complete, as for ordinary equivalences. We also prove that both results hold for CTL and LTL as well. We conclude the paper with some experimental results. In particular, we use our implementation to automatically prove the correctness of a set of six contextual equivalences of LTL recently introduced by Esparza et al. for the normalization of LTL formulas. While Esparza et al. need several pages of manual proof, our tool only needs milliseconds to do the job and to compute counterexamples for incorrect variants of the equivalences.

Cite as

Javier Esparza and Rubén Rubio. Validity of Contextual Formulas. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 24:1-24:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{esparza_et_al:LIPIcs.CONCUR.2024.24,
  author =	{Esparza, Javier and Rubio, Rub\'{e}n},
  title =	{{Validity of Contextual Formulas}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{24:1--24:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-339-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{311},
  editor =	{Majumdar, Rupak and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.24},
  URN =		{urn:nbn:de:0030-drops-207965},
  doi =		{10.4230/LIPIcs.CONCUR.2024.24},
  annote =	{Keywords: \mu-calculus, temporal logic, contextual rules}
}

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}
}

Search Results

Documents authored by Rubio, Rubén

Validity of Contextual Formulas

Abstract

Cite as

Model Checking Strategy-Controlled Rewriting Systems (System Description)

Abstract

Cite as

Thanks for your feedback!

Could not send message