10.46298/lmcs-18(4:6)2022
https://lmcs.episciences.org/9941
Wißmann, Thorsten
Thorsten
Wißmann
Milius, Stefan
Stefan
Milius
Schröder, Lutz
Lutz
Schröder
Quasilinear-time Computation of Generic Modal Witnesses for Behavioural Inequivalence
We provide a generic algorithm for constructing formulae that distinguish
behaviourally inequivalent states in systems of various transition types such
as nondeterministic, probabilistic or weighted; genericity over the transition
type is achieved by working with coalgebras for a set functor in the paradigm
of universal coalgebra. For every behavioural equivalence class in a given
system, we construct a formula which holds precisely at the states in that
class. The algorithm instantiates to deterministic finite automata, transition
systems, labelled Markov chains, and systems of many other types. The ambient
logic is a modal logic featuring modalities that are generically extracted from
the functor; these modalities can be systematically translated into custom sets
of modalities in a postprocessing step. The new algorithm builds on an existing
coalgebraic partition refinement algorithm. It runs in time $\mathcal{O}((m+n)
\log n)$ on systems with $n$ states and $m$ transitions, and the same
asymptotic bound applies to the dag size of the formulae it constructs. This
improves the bounds on run time and formula size compared to previous
algorithms even for previously known specific instances, viz. transition
systems and Markov chains; in particular, the best previous bound for
transition systems was $\mathcal{O}(m n)$.
Comment: arXiv admin note: substantial text overlap with arXiv:2105.00669
episciences.org
Computer Science - Logic in Computer Science
Attribution 4.0 International (CC BY 4.0)
2022-09-21
2022-11-17
2022-11-17
eng
journal article
arXiv:2203.11175
10.48550/arXiv.2203.11175
1860-5974
https://lmcs.episciences.org/9941/pdf
VoR
application/pdf
Logical Methods in Computer Science
Volume 18, Issue 4
Researchers
Students