Explaining Behavioural Inequivalence Generically in Quasilinear Time
Wißmann T, Milius S, Schröder L (2021)
Publication Type: Conference contribution
Publication year: 2021
Journal
Publisher: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Book Volume: 203
Conference Proceedings Title: Leibniz International Proceedings in Informatics, LIPIcs
Event location: Virtual, Online
ISBN: 9783959772037
DOI: 10.4230/LIPIcs.CONCUR.2021.32
Abstract
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 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 O(mn).
Authors with CRIS profile
Thorsten Wißmann
Stefan Milius Lehrstuhl für Informatik 8 (Theoretische Informatik) Lutz Schröder Lehrstuhl für Informatik 8 (Theoretische Informatik)
Stefan Milius Lehrstuhl für Informatik 8 (Theoretische Informatik) Lutz Schröder Lehrstuhl für Informatik 8 (Theoretische Informatik)
Involved external institutions
Netherlands (NL)How to cite
APA:
Wißmann, T., Milius, S., & Schröder, L. (2021). Explaining Behavioural Inequivalence Generically in Quasilinear Time. In Serge Haddad, Daniele Varacca (Eds.), Leibniz International Proceedings in Informatics, LIPIcs. Virtual, Online: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing.
MLA:
Wißmann, Thorsten, Stefan Milius, and Lutz Schröder. "Explaining Behavioural Inequivalence Generically in Quasilinear Time." Proceedings of the 32nd International Conference on Concurrency Theory, CONCUR 2021, Virtual, Online Ed. Serge Haddad, Daniele Varacca, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2021.
BibTeX: Download