Model checking the full modal mu-calculus for infinite sequential processes

被引：0
|
作者：
Burkart, O
Steffen, B
机构：
[1] Univ Edinburgh, JCMB, LFCS, Edinburgh EH9 3JZ, Midlothian, Scotland
[2] Univ Passau, FMI, D-94032 Passau, Germany
来源：
AUTOMATA, LANGUAGES AND PROGRAMMING | 1997年 / 1256卷
关键词：
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
In this paper we develop a new exponential algorithm for model-checking infinite sequential processes, including contest-free processes, pushdown processes, and regular graphs, that decides the full modal mu-calculus. Whereas the actual model checking algorithm results from considering conditional semantics together with backtracking caused by alternation, the corresponding correctness proof requires a stronger framework, which uses dynamic environments modelled by finite-state automata.
引用
收藏
页码：419 / 429
页数：11
相关论文
共 50 条
  • [21] Linear-time model-checking algorithm for the alternation-free modal mu-calculus
    Cleaveland, Rance, 1600, (02):
  • [22] An Infinitary Treatment of Full Mu-Calculus
    Afshari, Bahareh
    Jager, Gerhard
    Leigh, Graham E.
    LOGIC, LANGUAGE, INFORMATION, AND COMPUTATION (WOLLIC 2019), 2019, 11541 : 17 - 34
  • [23] Simple Probabilistic Extension of Modal Mu-Calculus
    Liu, Wanwei
    Song, Lei
    Wang, Ji
    Zhang, Lijun
    PROCEEDINGS OF THE TWENTY-FOURTH INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE (IJCAI), 2015, : 882 - 888
  • [24] CCS, LIVENESS, AND LOCAL MODEL CHECKING IN THE LINEAR TIME MU-CALCULUS
    STIRLING, C
    WALKER, D
    LECTURE NOTES IN COMPUTER SCIENCE, 1990, 407 : 166 - 178
  • [25] Heuristic search plus local model checking in selective mu-calculus
    Santone, A
    IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2003, 29 (06) : 510 - 523
  • [26] ON MODAL MU-CALCULUS AND BUCHI TREE AUTOMATA
    KAIVOLA, R
    INFORMATION PROCESSING LETTERS, 1995, 54 (01) : 17 - 22
  • [27] A modal mu-calculus for durational transition systems
    Seidl, H
    11TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 1996, : 128 - 137
  • [28] Simplifying the modal mu-calculus alternation hierarchy
    Bradfield, JC
    STACS 98 - 15TH ANNUAL SYMPOSIUM ON THEORETICAL ASPECTS OF COMPUTER SCIENCE, 1998, 1373 : 39 - 49
  • [29] Algorithmic correspondence for intuitionistic modal mu-calculus
    Conradie, Willem
    Fomatati, Yves
    Palmigiano, Alessandra
    Sourabh, Sumit
    THEORETICAL COMPUTER SCIENCE, 2015, 564 : 30 - 62
  • [30] The modal mu-calculus alternation hierarchy is strict
    Bradfield, JC
    THEORETICAL COMPUTER SCIENCE, 1998, 195 (02) : 133 - 153
12345