Coinduction Meets Algebra for the Axiomatization and Algorithmics of System Equivalences

共导与代数相结合，实现系统等价的公理化和算法

• 批准号: 259234802
• 负责人: Professor Dr. Stefan Milius
• 金额: --
• 依托单位: Informatik 8 - Theoretische Informatik
• 依托单位国家: 德国
• 项目类别: Research Grants
• 财政年份: 2014
• 资助国家: 德国
• 起止时间: 2013-12-31 至 2022-12-31
• 项目状态: 已结题
• 来源: https://gepris.dfg.de/gepris/projekt/259234802?language=en
• 关键词: Coinduction; Meets; Algebra; Axiomatization; Algorithmics

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.

等价性检验和状态空间最小化是时序和并发状态系统规范和验证中的重要任务。虽然这些任务通常是不可判定的，例如对于图灵完备的计算模型，但它们通常对于表达能力较低的模型仍然是可判定的。此外，对于这样的模型，通常可以使用公理化系统等价的语法表达式演算，例如经典确定性自动机的正则表达式和Kleene代数。对于有限状态系统的情况下，通用的表达式语言，公理化，和可判定性的结果是已知的，但实际的算法的等价性检查和最小化仍然是在个案的基础上对待。COAX的目标是开发通用算法的等价性检查和最小化的状态为基础的系统，参数化的过渡类型。第二个项目阶段将特别关注数据语言的名义系统和自动机。此外，我们将开发通用语言，推理系统和算法的规范和等价性检查的名义系统的状态空间是轨道有限的或代数有限的轨道有限集。在第一个项目阶段，我们将这些发展的基础上普遍余代数，它提供了一个统一的观点，广泛的状态为基础的系统，包括，除了经典的确定性或非确定性系统，例如加权的、概率的和基于游戏的系统。计划中的工作将联合收割机结合并扩展最近的几个研究方向，包括：共代数迹语义学;由Rutten等人发起并由申请人在项目第一阶段扩展的自动机及其理论的共代数一致化;在COAX第一阶段开发的双相似性下系统最小化的有效通用算法; Bonchi和Pous建议的互模拟直到同余技术; Silva等人研究的集合函子的共代数正则表达式演算;和理论的通用域的有限状态行为发起的申请人之一（Milius）。超越集理论的设置主要用于在以前的工作中，我们将工作在更一般的类别，特别是名义集和名义代数，以确保我们的通用语义理论和随后的统一算法的更广泛的适用性。我们将把我们的理论和算法实例化到选定的具体类型的系统中，包括名义系统和处理无限对象的系统。这将导致一个全面的机构的结果，结构和算法的等价性检查和最小化的广泛的系统类型。