Branching-time logics with path relativisation
Branching-time logics with path relativisation
复制标题
具有路径相对化的分支时间逻辑
DOI：
10.1016/j.jcss.2013.05.005
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
M. Lange
中科院分区：
文献类型：
--
作者：
M. Latte;M. Lange
我们定义了全分支时间时序逻辑 CTL⁎ 的扩展，其中路径量词通过无限单词的形式语言相对化，并考虑以相同方式扩展逻辑 CTL 和 CTL+ 获得的自然片段。这产生了一个小的二维时序逻辑层次结构，一方面由用于路径限制的语言类参数化，另一方面由时序运算符的使用参数化。我们通过两个应用场景来激发对此类逻辑的研究：在抽象和细化方面，它们提供了更精确的方法来排除虚假痕迹；它们在需要没有有限模型属性的可判定逻辑的软件综合中可能很有用。我们研究这些逻辑的相对表达能力以及它们的可满足性和模型检查问题的复杂性。
We define extensions of the full branching-time temporal logic CTL⁎in which the path quantifiers are relativised by formal languages of infinite words, and consider its natural fragments obtained by extending the logics CTL and CTL+in the same way. This yields a small and two-dimensional hierarchy of temporal logics parametrised by the class of languages used for the path restriction on one hand, and the use of temporal operators on the other. We motivate the study of such logics through two application scenarios: in abstraction and refinement they offer more precise means for the exclusion of spurious traces; and they may be useful in software synthesis where decidable logics without the finite model property are required. We study the relative expressive power of these logics as well as the complexities of their satisfiability and model-checking problems.
登录
查看更多内容
DOI：
10.1016/s0019-9958(82)91258-x
发表时间：
1982-07
期刊：
Inf. Control.
影响因子：
--
作者：
Robert S. Streett
通讯作者：
Robert S. Streett
模态定点逻辑求解器
DOI：
10.1016/j.entcs.2010.04.008
发表时间：
2010
期刊：
影响因子：
--
作者：
Oliver Friedmann;Martin Lange
通讯作者：
Martin Lange
CTL 和 CTL 之间指数简洁性差距的纯模型理论证明
影响因子：
0.5
作者：
M. Lange
通讯作者：
M. Lange
DOI：
10.1007/978-3-642-14203-1_28
发表时间：
2010-07
期刊：
--
影响因子：
--
作者：
Oliver Friedmann;Markus Latte;M. Lange
通讯作者：
Oliver Friedmann;Markus Latte;M. Lange
使用公平性使抽象发挥作用
影响因子：
1.8
作者：
D. Bosnacki;N. Ioustinova;N. Sidorova
通讯作者：
N. Sidorova