Higher-Level Synchronising Devices in Meije-SCCS
Higher-Level Synchronising Devices in Meije-SCCS
复制标题
DOI：
10.1016/0304-3975(85)90093-3
复制
发表时间：
1985
期刊：
影响因子：
--
通讯作者：
Robert de Simone
中科院分区：
文献类型：
--
作者：
Robert de Simone
在 R. Milner 提出的并行和同步代数设置中，我们定义了多种进程同步运算符。我们通过它们遵循的语义条件规则来介绍它们。我们证明它们是来自原始 SCCS 演算的高级非原始运算符，展示了如何用原始表达式来满足它们的行为。我们的目的是：研究表达性——要么是过渡系统领域的“语义”，要么是通过微积分中其他形式主义的翻译来研究“句法”。这些操作符允许人们指定处理（操作）产品和转换系统转换的正式复杂的同步模式，并且仍然不会失去其非正式的吸引人的直觉；因为我们然后忘记了与 Meije-SCCS 基本同步机制（引擎盖下的机制）一起工作的实现。除了组件动作幺半群上允许的关系之外，定义规则是在语法上给出的。这种“语义”方面使我们能够处理许多“可计算性”问题。对于封闭式术语尤其如此，我们可以在过渡系统中声称具有建设性的“普遍性”。运营商的情况似乎稍微复杂一些。我们的主要结果的证明使我们对开放表达式的等价证明进行了技术塑造，这本身就很有趣。
In an algebraic setting for parallelism and synchronisation due to R. Milner, we define a wide variety of synchronising operators on processes. We introduce them by the semanticalconditional rulesthey obey. We prove they are higher-level nonprimitive operators from the original SCCS calculus, showing how to meet their behaviours with primitive expressions. Our purposes are: study of expressiveness—either ‘semantic’, in the realm of transition systems, or ‘syntaxic’, through translation of other formalisms in the calculus. Such operators allow one to specify formally sophisticated synchronisation modes dealing with (operational) products and transformations of transition systems, and still not lose their informal appealing intuition; for we then forget the realisation working withMeije-SCCS elementary synchronisation mechanisms (the mechanics below the hood). The defining rules are syntactically given, except for the allowed relations on the components' actions monoids. This ‘semantical’ aspect allows us to treat many ‘calculability’ issues. This is especially true of closed terms, where we may claim constructive ‘universality’ amongst transition systems. The case of operators seems slightly more intricate. The proof of our main result has led us to a technical shaping of equivalence proofs for open expressions which shows to be interesting in its own right.