Ready simulation for concurrency: It's logical!
Ready simulation for concurrency: It's logical!
复制标题
DOI：
10.1016/j.ic.2010.02.001
复制
发表时间：
2007-07
期刊：
影响因子：
--
通讯作者：
G. Lüttgen;W. Vogler
中科院分区：
文献类型：
--
作者：
G. Lüttgen;W. Vogler
本文对货车Glabbeek的线性时间、分支时间谱的基于迹线的下半部分和基于模拟的上半部分之间的联系提供了新的见解。我们建立，准备好的模拟是完全抽象的故障包含，当添加的合取算子，作者在[TCS 373（1-2）19-40]的标准设置的标记的过渡系统（CSP风格）的并行组合。更确切地说，我们实际上证明了一个更强大的结果，考虑一个粗糙的关系比失败的包容性，即一个前序，涉及过程中可能出现的不一致，合取组合。准备模拟也显示，以满足标准的逻辑特性。此外，我们的语义形式主义证明了自己的强大时，添加析取，外部选择和隐藏操作，因此适合于研究混合操作和逻辑语言。最后，我们的形式主义的效用证明了一个小的例子，涉及飞机控制系统内的模式逻辑的指定和推理。
This article provides new insight into the connection between the trace-based lower part of van Glabbeek’s linear-time, branching-time spectrum and its simulation-based upper part. We establish that ready simulation is fully abstract with respect to failure inclusion, when adding the conjunction operator that was proposed by the authors in [TCS 373 (1–2) 19–40] to the standard setting of labelled transition systems with (CSP-style) parallel composition. More precisely, we actually prove a stronger result by considering a coarser relation than failure inclusion, namely a preorder that relates processes with respect to inconsistencies that may arise under conjunctive composition. Ready simulation is also shown to satisfy standard logic properties. In addition, our semantic formalism proves itself robust when adding disjunction, external choice and hiding operators, and is thus suited for studying mixed operational and logic languages. Finally, the utility of our formalism is demonstrated by means of a small example that deals with specifying and reasoning about mode logics within aircraft control systems.