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 条
  • [1] The μ-Calculus Model-Checking Algorithm for Generalized Possibilistic Decision Process
    Jiang, Jiulei
    Zhang, Panqing
    Ma, Zhanyou
    [J]. APPLIED SCIENCES-BASEL, 2020, 10 (07):
  • [2] Infinite state model-checking of propositional dynamic logics
    Goeller, Stefan
    Lohrey, Markus
    [J]. COMPUTER SCIENCE LOGIC, PROCEEDINGS, 2006, 4207 : 349 - 364
  • [3] Decomposition Theorems and Model-Checking for the Modal μ-Calculus
    Bojanczyk, Mikolaj
    Dittmann, Christoph
    Kreutzer, Stephan
    [J]. PROCEEDINGS OF THE JOINT MEETING OF THE TWENTY-THIRD EACSL ANNUAL CONFERENCE ON COMPUTER SCIENCE LOGIC (CSL) AND THE TWENTY-NINTH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS), 2014,
  • [4] Model-checking dense-time duration calculus
    Fränzle, M
    [J]. FORMAL ASPECTS OF COMPUTING, 2004, 16 (02) : 121 - 139
  • [5] Automatic abstraction techniques for propositional μ-calculus model checking
    Pardo, A
    Hachtel, GD
    [J]. COMPUTER AIDED VERIFICATION, 1997, 1254 : 12 - 23
  • [6] Model-Checking the Higher-DimensionalModal mu-calculus
    Lange, Martin
    Lozes, Etienne
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2012, (77): : 39 - 46
  • [7] Parallelizing a Symbolic Compositional Model-Checking Algorithm
    Cohen, Ariel
    Namjoshi, Kedar S.
    Sa'ar, Yaniv
    Zuck, Lenore D.
    Kisyova, Katya I.
    [J]. HARDWARE AND SOFTWARE: VERIFICATION AND TESTING, 2011, 6504 : 46 - +
  • [8] A LINEAR-TIME MODEL-CHECKING ALGORITHM FOR THE ALTERNATION-FREE MODAL MU-CALCULUS
    CLEAVELAND, R
    STEFFEN, B
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1992, 575 : 48 - 58
  • [9] A LINEAR-TIME MODEL-CHECKING ALGORITHM FOR THE ALTERNATION-FREE MODAL MU-CALCULUS
    CLEAVELAND, R
    STEFFEN, B
    [J]. FORMAL METHODS IN SYSTEM DESIGN, 1993, 2 (02) : 121 - 147
  • [10] Model-checking Web Services Orchestrations using BP-calculus
    Abouzaid, Faisal
    Mullins, John
    [J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 255 : 3 - 21
12345