Coalgebraic Model Checking

各种各样的时态逻辑在并发系统的响应特性规范中起着核心作用；它们允许灵活地表述需求，例如安全性、无死锁、活跃性和许多其他需求。并发程序和系统通常抽象地描述为有限转换系统。对上述类型的需求的验证随后表现为模型检查的问题，即需要算法来决定给定的时间公式在给定的转换系统中是否成立。这种算法和随后的验证工具的发展是一个科学和工业成熟的研究领域。典型地，转换系统是简单的关系结构。然而，如今，一系列更具表现力的模型正在被广泛使用。在这些模型中，系统演化涉及额外的特征，如概率、权重或基于博弈的现象。这就需要对这种行为进行建模的时间逻辑的变化，甚至是扩展，包括概率时间逻辑，Parikh的游戏逻辑和交替时间时间逻辑，仅举几个例子。CoMoC的目标是为这些系统开发通用的时间逻辑，以及用于模型检查的通用语义技术和算法方法。我们的泛型发展将建立在泛函子协代数的基础上，泛函子协代数是一个理论，它包含了各种各样的系统类型，超越了经典的纯关系世界，并且到目前为止，它提供了一个令人印象深刻的泛型结构理论结果，逻辑演算和算法技术，用于规范和验证基于状态的系统。在CoMoC中，我们将发展具有共代数一般性的一般分支时间逻辑和线性时间逻辑。特别是，我们将推进自动机和博弈论方法的最新技术，以进行模型检查，我们将增强逻辑的线性时间变量的通用性和适用性范围。此外，我们将重点关注数据语言和数据流的逻辑，以及具有计算副作用（如存储访问或堆栈操作）的响应式模型的逻辑。综上所述，我们将开发一个高度通用的模型检查框架，该框架在几个维度上是参数化的，包括系统类型、系统语义和计算能力。

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.