Document Open Access Logo

Coinductive Techniques for Checking Satisfiability of Generalized Nested Conditions

Authors Lara Stoltenow , Barbara König , Sven Schneider , Andrea Corradini , Leen Lambers , Fernando Orejas

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2024.39.pdf
  • Filesize: 0.87 MB
  • 20 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Program reasoning
Keywords
  • satisfiability
  • graph conditions
  • coinductive techniques
  • category theory

Metrics

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

Abstract

We study nested conditions, a generalization of first-order logic to a categorical setting, and provide a tableau-based (semi-decision) procedure for checking (un)satisfiability and finite model generation. This generalizes earlier results on graph conditions. Furthermore we introduce a notion of witnesses, allowing the detection of infinite models in some cases. To ensure completeness, paths in a tableau must be fair, where fairness requires that all parts of a condition are processed eventually. Since the correctness arguments are non-trivial, we rely on coinductive proof methods and up-to techniques that structure the arguments. We distinguish between two types of categories: categories where all sections are isomorphisms, allowing for a simpler tableau calculus that includes finite model generation; in categories where this requirement does not hold, model generation does not work, but we still obtain a sound and complete calculus.

Cite As Get BibTex

Lara Stoltenow, Barbara König, Sven Schneider, Andrea Corradini, Leen Lambers, and Fernando Orejas. Coinductive Techniques for Checking Satisfiability of Generalized Nested Conditions. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 39:1-39:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.CONCUR.2024.39

Author Details

Lara Stoltenow
  • University of Duisburg-Essen, Germany
Barbara König
  • University of Duisburg-Essen, Germany
Sven Schneider
  • Hasso Plattner Institute at the University of Potsdam, Germany
Andrea Corradini
  • Università di Pisa, Italy
Leen Lambers
  • Brandenburgische Technische Universität Cottbus-Senftenberg, Germany
Fernando Orejas
  • Universitat Politècnica de Catalunya, Spain

Funding

  • Corradini, Andrea: Research partially supported by the Italian MUR under the PRIN 20228KXFN2 "STENDHAL" and by the University of Pisa under the PRA 2022_99 "FM4HD".
  • Orejas, Fernando: Research partially supported by MCIN/ AEI /10.13039/501100011033 under grant PID2020-112581GB-C21.

References

  1. H.J. Sander Bruggink, Raphaël Cauderlier, Mathias Hülsbusch, and Barbara König. Conditional reactive systems. In Proc. of FSTTCS '11, volume 13 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011. URL: http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=3325.
  2. Bruno Courcelle. The monadic second-order logic of graphs I. Recognizable sets of finite graphs. Information and Computation, 85(1):12-75, 1990. Google Scholar
  3. Hartmut Ehrig, Karsten Ehrig, Ulrike Prange, and Gabriele Taentzer. Fundamentals of Algebraic Graph Transformation. Monographs in Theoretical Computer Science. Springer, 2006. Google Scholar
  4. Hartmut Ehrig and Barbara König. Deriving bisimulation congruences in the DPO approach to graph rewriting with borrowed contexts. MSCS, 16(6):1133-1163, 2006. Google Scholar
  5. Hartmut Ehrig, Michael Pfender, and Hans Jürgen Schneider. Graph grammars: An algebraic approach. In Proc. 14th IEEE Symp. on Switching and Automata Theory, pages 167-180, 1973. Google Scholar
  6. Melvin Fitting. First-Order Logic and Automated Theorem Proving. Springer, 1996. Google Scholar
  7. Peter J. Freyd and Andre Scedrov. Categories, Allegories. North-Holland, 1990. Google Scholar
  8. Annegret Habel and Karl-Heinz Pennemann. Correctness of high-level transformation systems relative to nested conditions. Mathematical Stuctures in Computer Science, 19(2):245-296, 2009. Google Scholar
  9. Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Kenneth L. McMillan. Abstractions from proofs. In Proc. of POPL '04, pages 232-244. ACM, 2004. Google Scholar
  10. Mathias Hülsbusch and Barbara König. Deriving bisimulation congruences for conditional reactive systems. In Proc. of FOSSACS '12, pages 361-375. Springer, 2012. LNCS/ARCoSS 7213. Google Scholar
  11. Mathias Hülsbusch, Barbara König, Sebastian Küpper, and Lara Stoltenow. Conditional Bisimilarity for Reactive Systems. Logical Methods in Computer Science, Volume 18, Issue 1, January 2022. URL: https://doi.org/10.46298/lmcs-18(1:6)2022.
  12. Stephen Lack and Paweł Sobociński. Adhesive and quasiadhesive categories. RAIRO - Theoretical Informatics and Applications, 39(3), 2005. Google Scholar
  13. Leen Lambers and Fernando Orejas. Tableau-based reasoning for graph properties. In Proc. of ICGT '14, pages 17-32. Springer, 2014. LNCS 8571. Google Scholar
  14. William Lawvere. Functorial Semantics of Algebraic Theories. PhD thesis, Columbia University, 1963. Google Scholar
  15. James J. Leifer. Operational congruences for reactive systems. PhD thesis, University of Cambridge Computer Laboratory, September 2001. Google Scholar
  16. James J. Leifer and Robin Milner. Deriving bisimulation congruences for reactive systems. In Proc. of CONCUR 2000, pages 243-258. Springer, 2000. LNCS 1877. Google Scholar
  17. Marisa Navarro, Fernando Orejas, Elvira Pino, and Leen Lambers. A navigational logic for reasoning about graph properties. Journal of Logical and Algebraic Methods in Programming, 118:100616, 2021. Google Scholar
  18. Karl-Heinz Pennemann. An algorithm for approximating the satisfiability problem of high-level conditions. In GT-VC@CONCUR, volume 213.1 of Electronic Notes in Theoretical Computer Science, pages 75-94. Elsevier, 2007. Google Scholar
  19. Karl-Heinz Pennemann. Development of Correct Graph Transformation Systems. PhD thesis, Universität Oldenburg, May 2009. Google Scholar
  20. Damien Pous. Complete lattices and up-to techniques. In Proc. of APLAS '07, pages 351-366. Springer, 2007. LNCS 4807. Google Scholar
  21. Damien Pous. Techniques modulo pour les bisimulations. PhD thesis, ENS Lyon, February 2008. URL: https://hal.archives-ouvertes.fr/tel-01441480.
  22. Damien Pous and Davide Sangiorgi. Enhancements of the coinductive proof method. In Davide Sangiorgi and Jan Rutten, editors, Advanced Topics in Bisimulation and Coinduction. Cambridge University Press, 2011. Google Scholar
  23. Arend Rensink. Representing first-order logic using graphs. In Proc. of ICGT '04, pages 319-335. Springer, 2004. LNCS 3256. Google Scholar
  24. Davide Sangiorgi. Introduction to Bisimulation and Coinduction. Cambridge University Press, 2011. Google Scholar
  25. Vladimiro Sassone and Paweł Sobociński. Reactive systems over cospans. In Proc. of LICS '05, pages 311-320. IEEE, 2005. Google Scholar
  26. Sven Schneider, Leen Lambers, and Fernando Orejas. Symbolic model generation for graph properties. In Proc. of FASE '17, pages 226-243. Springer, 2017. LNCS 10202. Google Scholar
  27. Paweł Sobociński. Deriving process congruences from reaction rules. PhD thesis, Department of Computer Science, University of Aarhus, 2004. Google Scholar
  28. Lara Stoltenow, Barbara König, Sven Schneider, Andrea Corradini, Leen Lambers, and Fernando Orejas. Coinductive techniques for checking satisfiability of generalized nested conditions, 2024. arXiv:2407.06864. URL: https://arxiv.org/abs/2407.06864.
  29. Alfred Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5:285-309, 1955. Google Scholar
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact