Coinduction Meets Algebra for the Axiomatization and Algorithmics of System Equivalences

• Applicants: Professor Dr. Stefan Milius; Professor Dr. Lutz Schröder
• Subject Area: Theoretical Computer Science
• Term: from 2014 to 2023
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 259234802

• Final Report Year: 2023

Final Report Abstract

State space minimization is an important task in the verification of state-based systems. Moreover, syntactic expression calculi axiomatizing equivalence of state-based systems are often available, e.g. regular expressions for standard finite automata. The object of COAX was to provide generic semantic foundations for the description of systems and algorithms for minimization and equivalence checking that are and their parametric in the transition type. These developments are based on universal coalgebra, which provides a uniform view of a wide range of state-based systems. In the second project phase COAX2, we have refined the modularity mechanisms and the complexity analysis of a partition refinement algorithm developed in the first project phase, and extended the genericity mechanisms of the algorithm to cover weighted systems. Moreover, we have implemented the algorithm in a generic and modular tool, the Coalgebraic Partition Refiner (CoPaR). The algorithm and the tool were subsequently extended into a fully fledged minimizer. Moreover, we have provided a generic algorithm, based on partition refinement, that computes distinguishing formulae for behaviourally inequivalent states. All these algorithms either match or improve the best known complexity in concrete instances. In work on generic expression calculi describing the behaviour of states of systems, we have shown that expression languages for branching-time semantics can be phrased as fragments of the coalgebraic µ-calculus. We thus recover a known result for the classical case of labelled transition systems, but also cover new instances such as weighted and probabilistic systems. In COAX, we have further developed a generic framework combining universal coalgebra and graded monads, in which the semantics of concurrency can be parametrized both over the branching type of the underlying transition systems and over the granularity of process equivalence. We thus capture spectra of behavioural equivalences, such as van Glabbeek’s classical linear-time / branching-time spectrum on labelled transition systems, in coalgebraic generality. This framework allows for the principled extraction of characteristic modal logics, for which we have proved Hennessy-Milner-type theorems. Finally, we have obtained results on the specification of varieties of finite algebraic structures, for which the classical Reiterman theorem provides a characterization by profinite equations. In COAX, we have developed a generic categorical approach to Reiterman’s theorem and the theory of profinite equations, working with monad algebras. It instantiates to the classical Reiterman Theorem as well as to a version for ordered algebras and a result for first-oder structures due to Pin and Weil.

Publications

• Predicate Liftings and Functor Presentations in Coalgebraic Expression Languages. Lecture Notes in Computer Science, 56-77.
  Dorsch, Ulrich; Milius, Stefan; Schröder, Lutz & Wißmann, Thorsten
  
• Generic Partition Refinement and Weighted Tree Automata. Lecture Notes in Computer Science, 280-297.
  Deifel, Hans-Peter; Milius, Stefan; Schröder, Lutz & Wißmann, Thorsten
  
• Graded monads and graded logics for the linear time - branching time spectrum. In Wan J. Fokkink and Rob van Glabbeek, eds., Concurrency Theory, CONCUR 2019, vol. 140 of LIPIcs, pp. 36:1–36:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019
  Ulrich Dorsch; Stefan Milius & Lutz Schröder
  
• Efficient and Modular Coalgebraic Partition Refinement. Logical Methods in Computer Science, Volume 16, Issue 1.
  Wißmann, Thorsten; Dorsch, Ulrich; Milius, Stefan & Schröder, Lutz
  
• Coalgebra encoding for efficient minimization. In Naoki Kobayashi, ed., Formal Structures for Computation and Deduction, FSCD 2021, vol. 195 of LIPIcs, pp. 28:1–28:19. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2021
  Hans-Peter Deifel; Stefan Milius & Thorsten Wißmann
  
• Explaining behavioural inequivalence generically in quasilinear time. In Serge Haddad and Daniele Varacca, eds., Concurrency Theory, CONCUR 2021, vol. 203 of LIPIcs, pp. 32:1–32:18. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2021
  Thorsten Wißmann; Stefan Milius & Lutz Schröder
  
• Finitary monads on the category of posets. Mathematical Structures in Computer Science, 31(7), 799-821.
  Adámek, Jiří; Ford, Chase; Milius, Stefan & Schröder, Lutz
  
• From generic partition refinement to weighted tree automata minimization. Formal Aspects of Computing, 33(4-5), 695-727.
  Wißmann, Thorsten; Deifel, Hans-Peter; Milius, Stefan & Schröder, Lutz
  
• Reiterman’s Theorem on Finite Algebras for a Monad. ACM Transactions on Computational Logic, 22(4), 1-48.
  Adámek, Jiří; Chen, Liang-Ting; Milius, Stefan & Urbat, Henning
  
• Quasilinear-time Computation of Generic Modal Witnesses for Behavioural Inequivalence. Logical Methods in Computer Science, Volume 18, Issue 4.
  Wißmann, Thorsten; Milius, Stefan & Schröder, Lutz