Computing Distinguishing Formulae for Threshold-Based Behavioural Distances
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866914326071214080 |
|---|---|
| author | Forster, Jonas Schröder, Lutz Wild, Paul König, Barbara Nora, Pedro |
| author_facet | Forster, Jonas Schröder, Lutz Wild, Paul König, Barbara Nora, Pedro |
| contents | Behavioural distances generally offer more fine-grained means of comparing quantitative systems than two-valued behavioural equivalences. They often relate to quantitative modalities, which generate quantitative modal logics that characterize a given behavioural distance in terms of the induced logical distance. We develop a unified framework for behavioural distances and logics induced by a special type of modalities that lift two-valued predicates to quantitative predicates. A typical example is the probability operator, which maps a two-valued predicate $A$ to a quantitative predicate on probability distributions assigning to each distribution the respective probability of $A$. Correspondingly, the prototypical example of our framework is $ε$-bisimulation distance of Markov chains, which has recently been shown to coincide with the behavioural distance induced by the popular Lévy-Prokhorov distance on distributions. Other examples include behavioural distance on metric transition systems and Hausdorff behavioural distance on fuzzy transition systems. Our main generic results concern the polynomial-time extraction of distinguishing formulae in two characteristic modal logics: A two-valued logic with a notion of satisfaction up to $ε$, and a quantitative modal logic. These results instantiate to new results in many of the mentioned examples. Notably, we obtain polynomial-time extraction of distinguishing formulae for $ε$-bisimulation distance of Markov chains in a quantitative logic featuring a `generally' modality used in probabilistic knowledge representation. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2602_12084 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Computing Distinguishing Formulae for Threshold-Based Behavioural Distances Forster, Jonas Schröder, Lutz Wild, Paul König, Barbara Nora, Pedro Logic in Computer Science 03B45, 03B50, 03B52, 03B70, 68Q10, 68Q85 F.4.1; F.1.2 Behavioural distances generally offer more fine-grained means of comparing quantitative systems than two-valued behavioural equivalences. They often relate to quantitative modalities, which generate quantitative modal logics that characterize a given behavioural distance in terms of the induced logical distance. We develop a unified framework for behavioural distances and logics induced by a special type of modalities that lift two-valued predicates to quantitative predicates. A typical example is the probability operator, which maps a two-valued predicate $A$ to a quantitative predicate on probability distributions assigning to each distribution the respective probability of $A$. Correspondingly, the prototypical example of our framework is $ε$-bisimulation distance of Markov chains, which has recently been shown to coincide with the behavioural distance induced by the popular Lévy-Prokhorov distance on distributions. Other examples include behavioural distance on metric transition systems and Hausdorff behavioural distance on fuzzy transition systems. Our main generic results concern the polynomial-time extraction of distinguishing formulae in two characteristic modal logics: A two-valued logic with a notion of satisfaction up to $ε$, and a quantitative modal logic. These results instantiate to new results in many of the mentioned examples. Notably, we obtain polynomial-time extraction of distinguishing formulae for $ε$-bisimulation distance of Markov chains in a quantitative logic featuring a `generally' modality used in probabilistic knowledge representation. |
| title | Computing Distinguishing Formulae for Threshold-Based Behavioural Distances |
| topic | Logic in Computer Science 03B45, 03B50, 03B52, 03B70, 68Q10, 68Q85 F.4.1; F.1.2 |
| url | https://arxiv.org/abs/2602.12084 |