Improved Algorithm of Global Model-Checking for Propositional μ-Calculus

被引：0
|
作者：
Jiang, Hua [1 ]
Xi, Jian-Qing [1 ]
机构：
[1] S China Univ Technol, Sch Comp Sci & Engn, Guangzhou 510640, Guangdong, Peoples R China
来源：
INFORMATION TECHNOLOGY APPLICATIONS IN INDUSTRY, PTS 1-4 | 2013年 / 263-266卷
关键词：
Model Checking; mu-Calculus; Computational complexity; NP boolean AND co-NP problem;
D O I：
10.4028/www.scientific.net/AMM.263-266.2314
中图分类号：
TP39 [计算机的应用];
学科分类号：
081203 ; 0835 ;
摘要：
Based on the research of the author when he was a Ph.D. student, he deeply studied the proposition of mu-Calculus, and used solving the partial ordering relation in formula mu-Calculus to solve formula mu-Calculus quickly. This paper improves and perfects the algorithm in reference [11]. The time complexity of the algorithm in this paper is O((2n+1)(left perpendicular d+2right perpendicular+1)), its space complexity is O(dn), where n is the number of states in the transition system and d is the nesting depth of fixpoint operators in the formula of proposition mu-Calculus.
引用
收藏
页码：2314 / 2319
页数：6
相关论文
共 50 条
  • [41] 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
  • [42] Model-checking Timed Temporal Logics
    Bouyer, Patricia
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 231 : 323 - 341
  • [43] Model-Checking HyperLTL for Pushdown Systems
    Pommellet, Adrien
    Touili, Tayssir
    MODEL CHECKING SOFTWARE, SPIN 2018, 2018, 10869 : 133 - 152
  • [44] A tool for model-checking Markov chains
    Holger Hermanns
    Joost-Pieter Katoen
    Joachim Meyer-Kayser
    Markus Siegle
    International Journal on Software Tools for Technology Transfer, 2003, 4 (2) : 153 - 172
  • [45] Foundations of incremental aspect model-checking
    Krishnamurthi, Shriram
    Fisler, Kathi
    ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY, 2007, 16 (02)
  • [46] Connectivity testing through model-checking
    Godskesen, JC
    Nielsen, B
    Skou, A
    FORMAL TECHNIQUES FOR NETWORKED AND DISTRIBUTED SYSTEMS - FORTE 2004, PROCEEDINGS, 2004, 3235 : 167 - 184
  • [47] Model-checking TRIO specifications in SPIN
    Morzenti, A
    Pradella, M
    San Pietro, P
    Spoletini, P
    FME 2003: FORMAL METHODS, PROCEEDINGS, 2003, 2805 : 542 - 561
  • [48] Model-checking access control policies
    Guelev, DP
    Ryan, M
    Schobbens, PY
    INFORMATION SECURITY, PROCEEDINGS, 2004, 3225 : 219 - 230
  • [49] On complexity of model-checking for the TQL logic
    Boneva, I
    Talbot, JM
    EXPLORING NEW FRONTIERS OF THEORETICAL INFORMATICS, 2004, 155 : 381 - 394
  • [50] A Model-Checking Tool for Families of Services
    Asirelli, Patrizia
    ter Beek, Maurice H.
    Fantechi, Alessandro
    Gnesi, Stefania
    FORMAL TECHNIQUES FOR DISTRIBUTED SYSTEMS, 2011, 6722 : 44 - 58
12345