Coalgebraic Model Checking

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

Various brands of temporal logics play a central role in the specification of reactive properties of concurrent systems; they allow for a flexible formulation of requirements such as safety, deadlock freedom, liveness, and many others. Concurrent programs and systems are typically described abstractly as finite transition systems. The verification of requirements of the mentioned kind then presents itself as the problem of model checking, i.e. one needs algorithms that decide whether a given temporal formula holds true in a given transition system. The development of such algorithms and ensuing verification tools is a scientifically and industrially well-established research area.Classically, transition systems are simple relational structures. 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 temporal logics for modelling such behaviour, including probabilistic temporal logics, Parikh's Game Logic, and alternating-time temporal logics, to name just a few examples. The goal of CoMoC is to develop generic temporal logics for such systems, along with generic semantic techniques and algorithmic methods for model-checking them. Our generic development will be founded on universal coalgebra, a theory which subsumes a wide variety of system types beyond the classical purely relational world under the notion of a functor coalgebra and which by now provides an impressive arsenal of generic structure theoretic results, logical calculi, and algorithmic techniques for the specification and verification of state-based systems.In CoMoC, we will develop generic branching-time as well as linear-time logics in coalgebraic generality. In partcular, we will advance the state of the art in automata- and game-theoretic approaches to model checking, and we will enhance the generality and range of applicability of linear-time variants of the logics. Additionally, we will focus on logics for data languages and data streams as well as logics for reactive models featuring computational side effects, such as store access or stack manipulation. Summing up, we will develop a highly generic model checking framework that is parametric along several dimensions including system type, system semantics, and computational power.