Coinduction Meets Algebra for the Axiomatization and Algorithmics of System Equivalences

等价性检查和状态空间最小化是顺序和并发状态系统规范和验证中的重要任务。虽然这些任务通常是不可确定的，例如对于图灵完备的计算模型，但对于表达能力较差的模型，它们通常仍然是可确定的。此外，对于这类模型，通常可以使用公理化系统等价的语法表达式演算，例如经典确定性自动机的正则表达式和Kleene代数。对于有限状态系统，一般表达式语言、公理化和可判定性结果是已知的，但是等价性检查和最小化的实际算法仍然是逐例处理的。COAX的目标是开发基于状态的系统的等价性检查和最小化的通用算法，在其转换类型中参数化。第二个项目阶段将特别侧重于数据语言的标称系统和自动机。此外，我们将开发通用语言、推理系统和算法，用于状态空间为轨道有限空间或轨道有限集上的代数有限空间的标称系统的规范和等价性检查。在第一个项目阶段，我们将把这些发展建立在通用协代数的基础上，它提供了广泛的基于状态的系统的统一视图，除了经典的确定性或非确定性系统外，还包括加权、概率和基于游戏的系统。计划中的工作将结合并扩展最近的几项研究，包括共代数迹语义；自动机的共代数均匀化及其理论，由Rutten等人发起，并在项目第一阶段由申请人扩展；COAX第一阶段开发的双相似条件下系统最小化的高效通用算法；Bonchi和Pous提出的双模拟一致性技术；Silva等人研究的集函子的共代数正则表达式演算以及由申请人之一（米利乌斯）发起的有限状态行为的一般域理论。超越先前工作中主要使用的集合论设置，我们将研究更一般的类别，特别是标称集合和标称代数，以确保我们的通用语义理论和随后的统一算法的更广泛的适用性。我们将实例化我们的理论和算法，以选择具体类型的系统，包括名义系统和系统处理无限对象。这将导致广泛的系统类型的等效性检查和最小化的结果，结构和算法的综合体。

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.