Coalgebraic Model Checking

代数模型检验

• 批准号: 419850228
• 负责人: Professor Dr. Stefan Milius
• 金额: --
• 依托单位: Informatik 8 - Theoretische Informatik
• 依托单位国家: 德国
• 项目类别: Research Grants
• 财政年份: 2019
• 资助国家: 德国
• 起止时间: 2018-12-31 至 2022-12-31
• 项目状态: 已结题
• 来源: https://gepris.dfg.de/gepris/projekt/419850228?language=en
• 关键词: 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.

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