Coinduction Meets Algebra for the Axiomatization and Algorithmics of System Equivalences

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

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.