Model Checking for the Full Hybrid Computation Tree Logic

被引：4
|
作者：
Kernberger, Daniel [1 ]
Lange, Martin [1 ]
机构：
[1] Univ Kassel, Sch Elect Engn & Comp Sci, Kassel, Germany
来源：
PROCEEDINGS 23RD INTERNATIONAL SYMPOSIUM ON TEMPORAL REPRESENTATION AND REASONING - TIME 2016 | 2016年
关键词：
TEMPORAL LOGIC; COMPLEXITY; FRAGMENTS;
D O I：
10.1109/TIME.2016.11
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
We consider the hybridisations of the full branching time logic CTL* through the addition of nominals, binders and jumps. We formally define three fragments restricting the interplay between hybrid operators and path formulae contrary to previous proposals in the literature which ignored potential problems with a formal semantics. We then investigate the model checking problem for these logics obtaining complexities from PSPACE-completeness to non-elementary decidability.
引用
收藏
页码：31 / 40
页数：10
相关论文
共 50 条
  • [1] Model checking quantified computation tree logic
    Rensink, Arend
    CONCUR 2006 - CONCURRENCY THEORY, PROCEEDINGS, 2006, 4137 : 110 - 125
  • [2] Model checking fuzzy computation tree logic
    Pan, Haiyu
    Li, Yongming
    Cao, Yongzhi
    Ma, Zhanyou
    FUZZY SETS AND SYSTEMS, 2015, 262 : 60 - 77
  • [3] VECTORIZED MODEL CHECKING FOR COMPUTATION TREE LOGIC
    HIRAISHI, H
    MEKI, S
    HAMAGUCHI, K
    LECTURE NOTES IN COMPUTER SCIENCE, 1991, 531 : 44 - 53
  • [4] Incremental model checking for fuzzy computation tree logic
    Pan, Haiyu
    Zhou, Jie
    Lin, Yuming
    Cao, Yongzhi
    FUZZY SETS AND SYSTEMS, 2025, 500
  • [5] Bounded model checking for probabilistic computation tree logic
    Zhou, Cong-Hua
    Liu, Zhi-Feng
    Wang, Chang-Da
    Ruan Jian Xue Bao/Journal of Software, 2012, 23 (07): : 1656 - 1668
  • [6] Quantum computation tree logic - Model checking and complete calculus
    Baltazar, P.
    Chadha, R.
    Mateus, P.
    INTERNATIONAL JOURNAL OF QUANTUM INFORMATION, 2008, 6 (02) : 219 - 236
  • [7] Model checking computation tree logic over finite lattices
    Pan, Haiyu
    Li, Yongming
    Cao, Yongzhi
    Ma, Zhanyou
    THEORETICAL COMPUTER SCIENCE, 2016, 612 : 45 - 62
  • [8] Computation tree logic model checking based on possibility measures
    Li, Yongming
    Li, Yali
    Ma, Zhanyou
    FUZZY SETS AND SYSTEMS, 2015, 262 : 44 - 59
  • [9] Polytime model checking for timed probabilistic computation tree logic
    Beauquier, D
    Slissenko, A
    ACTA INFORMATICA, 1998, 35 (08) : 645 - 664
  • [10] Polytime model checking for timed probabilistic computation tree logic
    Danièle Beauquier
    Anatol Slissenko
    Acta Informatica, 1998, 35 : 645 - 664
12345