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 条
  • [21] Talking model-checking technology
    Hoffman, Leah
    COMMUNICATIONS OF THE ACM, 2008, 51 (07) : 112 - 111
  • [22] Local model-checking of modal Mu-calculus on acyclic Labeled Transition Systems
    Mateescu, R
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANAYLSIS OF SYSTEMS, PROCEEDINGS, 2002, 2280 : 281 - 295
  • [23] Model-checking process equivalences
    Lange, Martin
    Lozes, Etienne
    Guzman, Manuel Vargas
    THEORETICAL COMPUTER SCIENCE, 2014, 560 : 326 - 347
  • [24] Model-Checking Iterated Games
    Huang, Chung-Hao
    Schewe, Sven
    Wang, Farn
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2013, 2013, 7795 : 154 - 168
  • [25] Model-checking for adventure videogames
    Moreno-Ger, Pablo
    Fuentes-Fernandez, Ruben
    Sierra-Rodriguez, Jose-Luis
    Fernandez-Manjon, Baltasar
    INFORMATION AND SOFTWARE TECHNOLOGY, 2009, 51 (03) : 564 - 580
  • [26] Symmetry reductions in model-checking
    Sistla, AP
    VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, 2003, 2575 : 25 - 25
  • [27] On model-checking of P systems
    Dang, Z
    Ibarra, OH
    Li, C
    Xie, GY
    UNCONVENTIONAL COMPUTATION, PROCEEDINGS, 2005, 3699 : 82 - 93
  • [28] Model-checking iterated games
    Chung-Hao Huang
    Sven Schewe
    Farn Wang
    Acta Informatica, 2017, 54 : 625 - 654
  • [29] Symbolic and Structural Model-Checking
    Thierry-Mieg, Yann
    FUNDAMENTA INFORMATICAE, 2021, 183 (3-4) : 319 - 342
  • [30] Model-Checking on Ordered Structures
    Eickmeyer, Kord
    van den Heuvel, Jan
    Kawarabayashi, Ken-ichi
    Kreutzer, Stephan
    de Mendez, Patrice Ossona
    Pilipczuk, Michal
    Quiroz, Daniel A.
    Rabinovich, Roman
    Siebertz, Sebastian
    ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2020, 21 (02)
12345