Document

# Validity of Contextual Formulas

## File

LIPIcs.CONCUR.2024.24.pdf
• Filesize: 0.84 MB
• 17 pages

## 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)
https://doi.org/10.4230/LIPIcs.CONCUR.2024.24

## 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.

## Subject Classification

##### ACM Subject Classification
• Theory of computation → Modal and temporal logics
##### Keywords
• μ-calculus
• temporal logic
• contextual rules

## Metrics

• Access Statistics
• Total Accesses (updated on a weekly basis)
0

## References

1. Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA336.
2. Julian C. Bradfield and Igor Walukiewicz. The mu-calculus and model checking. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking, pages 871-919. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-10575-8_26.
3. Edmund M. Clarke, Thomas A. Henzinger, and Helmut Veith. Introduction to model checking. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking, pages 1-26. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-10575-8_1.
4. Alexandre Duret-Lutz, Etienne Renault, Maximilien Colange, Florian Renkin, Alexandre Gbaguidi Aisse, Philipp Schlehuber-Caissier, Thomas Medioni, Antoine Martin, Jérôme Dubois, Clément Gillard, and Henrich Lauko. From Spot 2.0 to Spot 2.10: What’s new? In Sharon Shoham and Yakir Vizel, editors, Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part II, volume 13372 of Lecture Notes in Computer Science, pages 174-187. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-13188-2_9.
5. Niklas Eén and Niklas Sörensson. An extensible SAT-solver. In Enrico Giunchiglia and Armando Tacchella, editors, Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003. Santa Margherita Ligure, Italy, May 5-8, 2003 Selected Revised Papers, volume 2919 of Lecture Notes in Computer Science, pages 502-518. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-24605-3_37.
6. E. Allen Emerson. Temporal and modal logic. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, pages 995-1072. Elsevier and MIT Press, 1990. URL: https://doi.org/10.1016/B978-0-444-88074-1.50021-4.
7. E. Allen Emerson and Joseph Y. Halpern. Decision procedures and expressiveness in the temporal logic of branching time. J. Comput. Syst. Sci., 30(1):1-24, 1985. URL: https://doi.org/10.1016/0022-0000(85)90001-7.
8. Javier Esparza and Rubén Rubio. Validity of contextual formulas (extended version). arXiv, 2024. URL: https://doi.org/10.48550/arXiv.2407.07759.
9. Javier Esparza, Rubén Rubio, and Salomon Sickert. Efficient normalization of linear temporal logic. J. ACM, 71(2):16:1-16:42, 2024. URL: https://doi.org/10.1145/3651152.
10. Alexey Ignatiev, António Morgado, and João Marques-Silva. PySAT: A Python toolkit for prototyping with SAT oracles. In Olaf Beyersdorff and Christoph M. Wintersteiger, editors, Theory and Applications of Satisfiability Testing - SAT 2018 - 21st International Conference, SAT 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings, volume 10929 of Lecture Notes in Computer Science, pages 428-437. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-94144-8_26.
11. Nicola Prezza. CTL (Computation Tree Logic) SAT solver, 2014. URL: https://github.com/nicolaprezza/CTLSAT.
12. Rubén Rubio. Equivalence checker for contextual formulas. Software (visited on 2024-07-25). URL: https://github.com/ningit/ctxform.