Thorsten Wißmann ; Stefan Milius ; Lutz Schröder - Quasilinear-time Computation of Generic Modal Witnesses for Behavioural Inequivalence

lmcs:9941 - Logical Methods in Computer Science, November 17, 2022, Volume 18, Issue 4 - https://doi.org/10.46298/lmcs-18(4:6)2022
Quasilinear-time Computation of Generic Modal Witnesses for Behavioural InequivalenceArticle

Authors: Thorsten Wißmann ORCID; Stefan Milius ORCID; Lutz Schröder ORCID

    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).


    Volume: Volume 18, Issue 4
    Published on: November 17, 2022
    Accepted on: September 21, 2022
    Submitted on: August 19, 2022
    Keywords: Computer Science - Logic in Computer Science
    Funding:
      Source : OpenAIRE Graph
    • Grey-box learning of Interfaces for Refactoring Legacy Software (GIRLS); Funder: Netherlands Organisation for Scientific Research (NWO); Code: 612.001.852

    Consultation statistics

    This page has been seen 1531 times.
    This article's PDF has been downloaded 321 times.