Coinduction Meets Algebra for the Axiomatization and Algorithmics of System Equivalences

点击翻译按钮获取中文摘要

Equivalence checking and state space minimization are important tasks in the specification and verification of both sequential and concurrent state-based systems. While these tasks are in general undecidable, e.g. for Turing-complete models of computation, they often remain decidable for less expressive models. Moreover, for such models, syntactic expression calculi axiomatizing system equivalence are often available, e.g. regular expressions and Kleene algebra for classical deterministic automata. For the case of finite-state systems, generic expression languages, axiomatizations, and decidability results are known, but the actual algorithmics of equivalence checking and minimization is still treated on a case by case basis. The goal of COAX is to develop generic algorithms for equivalence checking and minimization of state-based systems, parametrically in their transition type. The second project phase will particularly focus on nominal systems and automata for data languages. Furthermore, we will develop generic languages, reasoning systems and algorithms for the specification and equivalence checking of nominal systems whose state spaces are orbit-finite or algebraically finitary over orbit finite sets.As in the first project phase, we will base these developments on universal coalgebra, which provides a uniform view of a wide range of state-based systems including, besides classical deterministic or non-deterministic systems, e.g. weighted, probabilistic, and game-based systems. The planned work will combine and extend several recent strands of research including coalgebraic trace semantics; the coalgebraic uniformization of automata and their theory initiated by Rutten et al. and extended by the applicants in the first phase of the project; efficient generic algorithms for minimization of systems under bisimilarity as developed in the first phase of COAX; bisimulation up-to-congruence techniques as suggested by Bonchi and Pous; coalgebraic regular expression calculi for set functors as studied by Silva et al.; and a theory of generic domains of finite state behaviour initiated by one of the applicants (Milius).Going beyond the set-theoretic setting predominantly used in previous work, we will work over more general categories, in particular nominal sets and nominal algebras, in order to ensure wider applicability of our generic semantic theory and the ensuing uniform algorithms. We will instantiate our theory and algorithms to selected concrete types of systems, including nominal systems and systems processing infinite objects. This will lead to a comprehensive body of results, constructions, and algorithms for equivalence checking and minimization of a wide range of system types.