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 条
  • [31] Model-checking -: A tutorial introduction
    Müller-Olm, M
    Schmidt, D
    Steffen, B
    STATIC ANALYSIS, 1999, 1694 : 330 - 354
  • [32] Model-checking with coverability graphs
    Schmidt, K
    FORMAL METHODS IN SYSTEM DESIGN, 1999, 15 (03) : 239 - 254
  • [33] Model-checking processes with data
    Groote, JF
    Willemse, TAC
    SCIENCE OF COMPUTER PROGRAMMING, 2005, 56 (03) : 251 - 273
  • [34] Model-checking hierarchical structures
    Lohrey, M
    LICS 2005: 20TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE - PROCEEDINGS, 2005, : 168 - 177
  • [35] Model-Checking with Coverability Graphs
    Karsten Schmidt
    Formal Methods in System Design, 1999, 15 : 239 - 254
  • [36] Model-Checking of Smart Contracts
    Nehai, Zeinab
    Piriou, Pierre-Yves
    Daumas, Frederic
    IEEE 2018 INTERNATIONAL CONGRESS ON CYBERMATICS / 2018 IEEE CONFERENCES ON INTERNET OF THINGS, GREEN COMPUTING AND COMMUNICATIONS, CYBER, PHYSICAL AND SOCIAL COMPUTING, SMART DATA, BLOCKCHAIN, COMPUTER AND INFORMATION TECHNOLOGY, 2018, : 980 - 987
  • [37] Model-checking iterated games
    Huang, Chung-Hao
    Schewe, Sven
    Wang, Farn
    ACTA INFORMATICA, 2017, 54 (07) : 625 - 654
  • [38] Model-Checking Process Equivalences
    Lange, Martin
    Lozes, Etienne
    Guzman, Manuel Vargas
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2012, (96): : 43 - 56
  • [39] Model-checking hierarchical structures
    Lohrey, Markus
    JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 2012, 78 (02) : 461 - 490
  • [40] Verifying Business Rules Using Model-Checking Techniques for Non-specialist in Model-Checking
    Aoki, Yoshitaka
    Matsuura, Saeko
    IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS, 2014, E97D (05) : 1097 - 1108
12345