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 条
  • [41] Effective Cut-elimination for a Fragment of Modal mu-calculus
    Grigori Mints
    Studia Logica, 2012, 100 : 279 - 287
  • [42] Relating Paths in Transition Systems: The Fall of the Modal Mu-Calculus
    Dima, Catalin
    Maubert, Bastien
    Pinchinat, Sophie
    MATHEMATICAL FOUNDATIONS OF COMPUTER SCIENCE 2015, PT I, 2015, 9234 : 179 - 191
  • [43] Relating Paths in Transition Systems: The Fall of the Modal Mu-Calculus
    Dima, Catalin
    Maubert, Bastien
    Pinchinat, Sophie
    ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2018, 19 (03)
  • [44] Bounded game-theoretic semantics for modal mu-calculus
    Hella, Lauri
    Kuusisto, Antti
    Ronnholm, Raine
    INFORMATION AND COMPUTATION, 2022, 289
  • [45] Spatial logic of tangled closure operators and modal mu-calculus
    Goldblatt, Robert
    Hodkinson, Ian
    ANNALS OF PURE AND APPLIED LOGIC, 2017, 168 (05) : 1032 - 1090
  • [46] Extension of synthesis algorithm of recursive processes to mu-calculus
    Kimura, S
    Togashi, A
    Shiratori, N
    INFORMATION PROCESSING LETTERS, 1996, 58 (02) : 97 - 104
  • [47] Efficient on-the-fly model-checking for regular alternation-free mu-calculus
    Mateescu, R
    Sighireanu, M
    SCIENCE OF COMPUTER PROGRAMMING, 2003, 46 (03) : 255 - 281
  • [48] Uniform Interpolation from Cyclic Proofs: The Case of Modal Mu-Calculus
    Afshari, Bahareh
    Leigh, Graham E.
    Turata, Guillermo Menendez
    AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS, TABLEAUX 2021, 2021, 12842 : 335 - 353
  • [49] Modal Mu-calculus Extension with Description of Autonomy and Its Algebraic Structure
    Yamasaki, Susumu
    Sasakura, Mariko
    PROCEEDINGS OF THE 5TH INTERNATIONAL CONFERENCE ON COMPLEXITY, FUTURE INFORMATION SYSTEMS AND RISK (COMPLEXIS), 2020, : 63 - 71
  • [50] UppDMC: A Distributed Model Checker for Fragments of the mu-Calculus
    Holmem, Fredrik
    Leucker, Martin
    Lindstrom, Marcus
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2005, 128 (03) : 91 - 105
12345