3 LOGICS FOR BRANCHING BISIMULATION
3 LOGICS FOR BRANCHING BISIMULATION
复制标题
DOI：
10.1145/201019.201032
复制
发表时间：
1995-03-01
影响因子：
2.5
通讯作者：
VAADRAGER, F
中科院分区：
文献类型：
--
作者：
DENICOLA, R;VAADRAGER, F
引入了三种时间逻辑，它们在标记的转换系统上诱导出与分支互模拟相同的标识，这是一种行为等效性，旨在忽略不可见的转换，同时保留系统的分支结构。第一个逻辑是Hennessy-Milner逻辑的扩展，带有“until”运算符。第二个是Hennessy-Milner逻辑的另一个扩展，它利用了向后模态的力量。第三种逻辑是没有下一次运算符的CTL*。最后一个特征的一个相关副作用是，它在基于状态和基于动作的方法之间架起了一座桥梁，以实现并发系统的语义。
Three temporal logics are introduced that induce on labeled transition systems the same identifications as branching bisimulation, a behavioral equivalence that aims at ignoring invisible transitions while preserving the branching structure of systems. The first logic is an extension of Hennessy-Milner Logic with an ''until'' operator. The second one is another extension of Hennessy-Milner Logic, which exploits the power of backward modalities. The third logic is CTL* without the next-time operator. A relevant side-effect of the last characterization is that it sets a bridge between the state- and action-based approaches to the semantics of concurrent systems.