Expressive Logics for Coinductive Predicates
The classical Hennessy-Milner theorem says that two states of an image-finite transition system are bisimilar if and only if they satisfy the same formulas in a certain modal logic. In this paper we study this type of result in a general context, moving from transition systems to coalgebras and from...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2021-12-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/6593/pdf |
| _version_ | 1797268472747524096 |
|---|---|
| author | Clemens Kupke Jurriaan Rot |
| author_facet | Clemens Kupke Jurriaan Rot |
| author_sort | Clemens Kupke |
| collection | DOAJ |
| description | The classical Hennessy-Milner theorem says that two states of an image-finite
transition system are bisimilar if and only if they satisfy the same formulas
in a certain modal logic. In this paper we study this type of result in a
general context, moving from transition systems to coalgebras and from
bisimilarity to coinductive predicates. We formulate when a logic fully
characterises a coinductive predicate on coalgebras, by providing suitable
notions of adequacy and expressivity, and give sufficient conditions on the
semantics. The approach is illustrated with logics characterising similarity,
divergence and a behavioural metric on automata. |
| first_indexed | 2024-04-25T01:33:02Z |
| format | Article |
| id | doaj.art-1550e8d40aaf4eb8a7de5dc4bbbc50eb |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:33:02Z |
| publishDate | 2021-12-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-1550e8d40aaf4eb8a7de5dc4bbbc50eb2024-03-08T10:35:55ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742021-12-01Volume 17, Issue 410.46298/lmcs-17(4:19)20216593Expressive Logics for Coinductive PredicatesClemens Kupkehttps://orcid.org/0000-0002-0502-391XJurriaan RotThe classical Hennessy-Milner theorem says that two states of an image-finite transition system are bisimilar if and only if they satisfy the same formulas in a certain modal logic. In this paper we study this type of result in a general context, moving from transition systems to coalgebras and from bisimilarity to coinductive predicates. We formulate when a logic fully characterises a coinductive predicate on coalgebras, by providing suitable notions of adequacy and expressivity, and give sufficient conditions on the semantics. The approach is illustrated with logics characterising similarity, divergence and a behavioural metric on automata.https://lmcs.episciences.org/6593/pdfcomputer science - logic in computer science |
| spellingShingle | Clemens Kupke Jurriaan Rot Expressive Logics for Coinductive Predicates Logical Methods in Computer Science computer science - logic in computer science |
| title | Expressive Logics for Coinductive Predicates |
| title_full | Expressive Logics for Coinductive Predicates |
| title_fullStr | Expressive Logics for Coinductive Predicates |
| title_full_unstemmed | Expressive Logics for Coinductive Predicates |
| title_short | Expressive Logics for Coinductive Predicates |
| title_sort | expressive logics for coinductive predicates |
| topic | computer science - logic in computer science |
| url | https://lmcs.episciences.org/6593/pdf |
| work_keys_str_mv | AT clemenskupke expressivelogicsforcoinductivepredicates AT jurriaanrot expressivelogicsforcoinductivepredicates |