Document Open Access Logo

Hennessy-Milner Theorems via Galois Connections

Authors Harsh Beohar, Sebastian Gurke, Barbara König, Karla Messing

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2023.12.pdf
  • Filesize: 0.69 MB
  • 18 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Concurrency
  • Theory of computation → Modal and temporal logics
Keywords
  • behavioural equivalences and metrics
  • modal logics
  • Galois connections

Metrics

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

Abstract

We introduce a general and compositional, yet simple, framework that allows to derive soundness and expressiveness results for modal logics characterizing behavioural equivalences or metrics (also known as Hennessy-Milner theorems). It is based on Galois connections between sets of (real-valued) predicates on the one hand and equivalence relations/metrics on the other hand and covers a part of the linear-time-branching-time spectrum, both for the qualitative case (behavioural equivalences) and the quantitative case (behavioural metrics). We derive behaviour functions from a given logic and give a condition, called compatibility, that characterizes under which conditions a logically induced equivalence/metric is induced by a fixpoint equation. In particular, this framework allows to derive a new fixpoint characterization of directed trace metrics.

Cite As Get BibTex

Harsh Beohar, Sebastian Gurke, Barbara König, and Karla Messing. Hennessy-Milner Theorems via Galois Connections. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 12:1-12:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.CSL.2023.12

Author Details

Harsh Beohar
  • University of Sheffield, UK
Sebastian Gurke
  • Universität Duisburg-Essen, Germany
Barbara König
  • Universität Duisburg-Essen, Germany
Karla Messing
  • Universität Duisburg-Essen, Germany

Funding

The first author was partially supported by the EPSRC NIA Grant EP/X019373/1, while the remaining authors were partially supported by the DFG project SpeQt.

Acknowledgements

We want to thank Jonas Forster, Lutz Schröder and Paul Wild for several interesting discussions on the topics of this paper.

References

  1. Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König. Coalgebraic behavioral metrics. Logical Methods in Computer Science, 14(3), 2018. Selected Papers of the 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Google Scholar
  2. Paolo Baldan, Barbara König, and Tommaso Padoan. Abstraction, up-to techniques and games for systems of fixpoint equations. In Proc. of CONCUR '20, volume 171 of LIPIcs, pages 25:1-25:20. Schloss Dagstuhl - Leibniz Center for Informatics, 2020. Google Scholar
  3. Harsh Beohar, Sebastian Gurke, Barbara König, and Karla Messing. Hennessy-Milner theorems via Galois connections, 2022. URL: http://arxiv.org/abs/2207.05407.
  4. Patrick Cousot and Radhia Cousot. Systematic design of program analysis frameworks. In Proc. of POPL '79 (San Antonio, Texas), pages 269-282. ACM Press, 1979. Google Scholar
  5. Patrick Cousot and Radhia Cousot. Temporal abstract interpretation. In Mark N. Wegman and Thomas W. Reps, editors, Proc. of POPL '00, pages 12-25. ACM, 2000. Google Scholar
  6. Luca de Alfaro, Marco Faella, and Mariëlle Stoelinga. Linear and branching system metrics. IEEE Transactions on Software Engineering, 35(2):258-273, 2009. Google Scholar
  7. Josée Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden. Metrics for labelled Markov processes. Theoretical Computer Science, 318:323-354, 2004. Google Scholar
  8. Uli Fahrenberg and Axel Legay. The quantitative linear-time-branching-time spectrum. Theoretical Computer Science, 538:54-69, 2014. Google Scholar
  9. Matthew Hennessy and Robin Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32:137-161, 1985. Google Scholar
  10. Bart Jacobs. Categorical Logic and Type Theory, volume 141 of Studies in Logic and the Foundations of Mathematics. Elsevier, 1st edition, January 1999. Google Scholar
  11. Bartek Klin. The least fibred lifting and the expressivity of coalgebraic modal logic. In Proc. of CALCO '05, pages 247-262. Springer, 2005. LNCS 3629. Google Scholar
  12. Bartek Klin. Coalgebraic modal logic beyond sets. In Proc. of MFPS '07, volume 173 of ENTCS, pages 177-201, 2007. Google Scholar
  13. Bartosz Klin. An Abstract Coalgebraic Approach to Process Equivalence for Well-Behaved Operational Semantics. PhD thesis, University of Aarhus, 2004. Google Scholar
  14. Yuichi Komorida, Shin-ya Katsumata, Clemens Kupke, Jurriaan Rot, and Ichiro Hasuo. Expressivity of quantitative modal logics: Categorical foundations via codensity and approximation. In Proc. LICS '21, pages 1-14. IEEE, 2021. Google Scholar
  15. Barbara König and Christina Mika-Michalski. (Metric) bisimulation games and real-valued modal logics for coalgebras. In Proc. of CONCUR '18, volume 118 of LIPIcs, pages 37:1-37:17. Schloss Dagstuhl - Leibniz Center for Informatics, 2018. Google Scholar
  16. Antonín Kucera and Javier Esparza. A logical viewpoint on process-algebraic quotients. Journal of Logic and Computation, 13(6):863-880, 2003. Google Scholar
  17. Clemens Kupke and Dirk Pattinson. Coalgebraic semantics of modal logics: An overview. Theoretical Computer Science, 412:5070-5094, 2011. Google Scholar
  18. Clemens Kupke and Jurriaan Rot. Expressive logics for coinductive predicates. In Proc. of CSL '20, volume 152 of LIPIcs, pages 26:1-26:18. Schloss Dagstuhl - Leibniz Center for Informatics, 2020. Google Scholar
  19. George Markowsky. Chain-complete posets and directed sets with applications. Algebra Universalis, 6(1):53-68, 1976. Google Scholar
  20. E. J. McShane. Extension of range of functions. Bull. Amer. Math. Soc., 40(12):837-842, 1934. Google Scholar
  21. Stefan Milius, Dirk Pattinson, and Lutz Schröder. Generic trace semantics and graded monads. In Proc. of CALCO '15, volume 35 of LIPIcs, pages 253-269. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. Google Scholar
  22. Dusko Pavlovic, Michael Mislove, and James Worrell. Testing semantics: Connecting processes and process logics. In Proc. of AMAST '06, pages 308-322. Springer, 2006. LNCS 4019. Google Scholar
  23. Damien Pous. Complete lattices and up-to techniques. In Proc. of APLAS '07, pages 351-366. Springer, 2007. LNCS 4807. Google Scholar
  24. Franck van Breugel and James Worrell. A behavioural pseudometric for probabilistic transition systems. Theoretical Computer Science, 331:115-142, 2005. Google Scholar
  25. Rob van Glabbeek. The linear time - branching time spectrum I. In J.A. Bergstra, A. Ponse, and S.A. Smolka, editors, Handbook of Process Algebra, chapter 1, pages 3-99. Elsevier, 2001. Google Scholar
  26. Hassler Whitney. Analytic extensions of differentiable functions defined in closed sets. Transactions of the American Mathematical Society, 36(1):63-89, 1934. 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