We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LO

Change to browse by:

cs

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: Hennessy-Milner Theorems via Galois Connections

Abstract: We introduce a general and compositional, yet simple, framework that allows us 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 us to derive a new fixpoint characterization of directed trace metrics.
Subjects: Logic in Computer Science (cs.LO)
Cite as: arXiv:2207.05407 [cs.LO]
  (or arXiv:2207.05407v2 [cs.LO] for this version)

Submission history

From: Barbara König [view email]
[v1] Tue, 12 Jul 2022 09:16:59 GMT (203kb,D)
[v2] Wed, 20 Jul 2022 13:15:42 GMT (204kb,D)

Link back to: arXiv, form interface, contact.