Coalgebraic Model Checking (CoMoC2)

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

One of the central tasks in system verification is model checking, i.e. to determine whether or not a given model of a piece of software or hardware satisfies a given specification. Here, a specification may be expressed either as a formula in a dedicated temporal logic or as another system which the system under verification is required to refine a suitable sense. Such formalisms typically allow the formulation of requirements such as safety, deadlock freedom, liveness, and many others. Model checking in this sense presents a range of algorithmic problems concerning the complexity of model checking as well as the development of efficient model checking algorithms and their implementation in automated verification tools; as such, model checking constitutes a scientifically and industrially well-established research area. Classically, the models to be checked take the shape of simple relational transition systems. Nowadays, however, a range of more expressive models is being widely used. In these models, the system evolution involves additional features, such as probabilities, weights, or game-based phenomena. This entails a variation, and indeed a proliferation, of specification formalisms for such behavior; prominent examples of non-relational temporal logics include probabilistic temporal logics, game logic, and alternating-time temporal logics. The goal of CoMoC is to provide generic formalisms, methods, and algorithms for the unified treatment of model checking across system types and system semantics. To this end, we work with a parametrization of the overall framework over several key aspects. In particular, we encapsulate the system type as a set functor following the paradigm of universal coalgebra, we abstract over the semantics of next-step modalities using methods of coalgebraic logic, and we abstract over the granularity of system semantics on generalized linear-time / branching-time spectra using graded monads. In the second project phase CoMoC2, we will extend the scope of the generic theory and the associated algorithms and tools, aiming, in particular, to develop efficient model-checking algorithms for alternation-free fixpoint logics as well as techniques for bounded and symbolic model checking over coalgebraic systems. Additionally, we will focus on representations of coalgebraic models in terms of generic expression languages in the style of process algebra. Subsequent to this, a further emphasis in the second project phase will be on the above-mentioned perspective on model checking as expression refinement in the style used classically for certain process algebras such as CSP. Summing up, we aim to develop a body of highly generic model representation languages and specification logics, along with associated model checking algorithms and tools, that are parametrized over the type of systems as well as the granularity of the underlying behavioral equivalence.

• DFG Programme: Research Grants