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 条
  • [31] A Proof System with Names for Modal Mu-calculus
    Stirling, Colin
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2013, (129): : 18 - 29
  • [32] Fast Mu-calculus model checking when tree-width is bounded
    Obdrzálek, J
    COMPUTER AIDED VERIFICATION, 2003, 2725 : 80 - 92
  • [33] An Expressive Timed Modal Mu-Calculus for Timed Automata
    Cleaveland, Rance
    Keiren, Jeroen J. A.
    Fontana, Peter
    QUANTITATIVE EVALUATION OF SYSTEMS AND FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS, QEST-FORMATS 2024, 2024, 14996 : 160 - 178
  • [34] Probabilistic temporal logics via the modal mu-calculus
    Narasimha, M
    Cleaveland, R
    Iyer, P
    FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, 1999, 1578 : 288 - 305
  • [35] Cut-free Completeness for Modal Mu-Calculus
    Afshari, Bahareh
    Leigh, Graham E.
    2017 32ND ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS), 2017,
  • [36] Probabilistic temporal logics via the modal mu-calculus
    Cleaveland, R
    Iyer, SP
    Narasimha, M
    THEORETICAL COMPUTER SCIENCE, 2005, 342 (2-3) : 316 - 350
  • [37] Effective Cut-elimination for a Fragment of Modal mu-calculus
    Mints, Grigori
    STUDIA LOGICA, 2012, 100 (1-2) : 279 - 287
  • [38] PROOF SYSTEMS FOR TWO-WAY MODAL MU-CALCULUS
    Afshari, Bahareh
    Enqvist, Sebastian
    Leigh, Graham e.
    Marti, Johannes
    Venema, Yde
    JOURNAL OF SYMBOLIC LOGIC, 2023,
  • [39] Syntactic cut-elimination for a fragment of the modal mu-calculus
    Bruennler, Kai
    Studer, Thomas
    ANNALS OF PURE AND APPLIED LOGIC, 2012, 163 (12) : 1838 - 1853
  • [40] Partial-order reduction in the weak modal mu-calculus
    Ramakrishna, YS
    Smolka, SA
    CONCUR'97 : CONCURRENCY THEORY, 1997, 1243 : 5 - 24
12345