A process algebraic view of I/O automata
A process algebraic view of I/O automata
复制标题
I/O 自动机的过程代数视图
DOI：
10.1007/s00165-007-0066-z
复制
发表时间：
1992
影响因子：
1
通讯作者：
R. Segala
中科院分区：
文献类型：
--
作者：
R. Segala
Lynch 和 Tuttle 的输入/输出自动机形式是一种广泛使用的并发算法规范和验证框架。不幸的是，它从未被提供过代数表征，而这种形式化对于 CSP、CCS 和 ACP 等理论的成功至关重要。我们提出了 I/O 自动机的多种分类代数，其中考虑了接口、输入启用和本地控制等概念。它具有足够的表达能力来表示所有有限分支转移系统，因此所有 I/O 自动机都具有有限分支转移关系。我们的演示包括对带有输入和输出的无递归过程的静态先序关系的完整公理化。最后，我们给出了一些示例规范，并使用它们来展示基于我们的代数方法的验证方法。
The Input/Output Automata formalism of Lynch and Tuttle is a widely used framework for the specification and verification of concurrent algorithms. Unfortunately, it has never been provided with an algebraic characterization, a formalization which has been fundamental for the success of theories like CSP, CCS and ACP. We present a many-sorted algebra for I/O Automata that takes into account notions such as interface, input enabling, and local control. It is sufficiently expressive for representing all finitely branching transition systems, hence all I/O automata with a finitely branching transition relation. Our presentation includes a complete axiomatization of the quiescent preorder relation over recursion free processes with input and output. Finally, we give some example specifications and use them to show the methodology of verification based on our algebraic approach.