A LINEAR-TIME MODEL-CHECKING ALGORITHM FOR THE ALTERNATION-FREE MODAL MU-CALCULUS

被引:73
|
作者
CLEAVELAND, R
STEFFEN, B
机构
[1] N CAROLINA STATE UNIV, DEPT COMP SCI, RALEIGH, NC 27695 USA
[2] RHEIN WESTFAL TH AACHEN, LEHRSTUHL INFORMAT 2, W-5100 AACHEN, GERMANY
关键词
FORMAL METHODS IN SYSTEM ANALYSIS; AUTOMATED VERIFICATION; MODEL-CHECKING ALGORITHMS;
D O I
10.1007/BF01383878
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
We develop a model-checking algorithm for a logic that permits propositions to be defined using greatest and least fixed points of mutually recursive systems of equations. This logic is as expressive as the alternation-free fragment of the modal mu-calculus identified by Emerson and Lei, and it may therefore be used to encode a number of temporal logics and behavioral preorders. Our algorithm determines whether a process satisfies a formula in time proportional to the product of the sizes of the process and the formula; this improves on the best known algorithm for similar fixed-point logics.
引用
收藏
页码:121 / 147
页数:27
相关论文
共 50 条
  • [41] Symbolic model checking temporal logics of knowledge in multi-agent system via extended mu-calculus
    Wu, Lijun
    Su, Jinshu
    [J]. BIO-INSPIRED COMPUTATIONAL INTELLIGENCE AND APPLICATIONS, 2007, 4688 : 510 - +
  • [42] BRANCHING TIME REGULAR TEMPORAL LOGIC FOR MODEL CHECKING WITH LINEAR-TIME COMPLEXITY
    HAMAGUCHI, K
    HIRAISHI, H
    YAJIMA, S
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1991, 531 : 253 - 262
  • [43] Model checking of linear-time properties in multi-valued systems
    Li, Yongming
    Droste, Manfred
    Lei, Lihui
    [J]. INFORMATION SCIENCES, 2017, 377 : 51 - 74
  • [44] BFS-Based Model Checking of Linear-Time Properties with an Application on GPUs
    Wijs, Anton
    [J]. COMPUTER AIDED VERIFICATION: 28TH INTERNATIONAL CONFERENCE, CAV 2016, PT II, 2016, 9780 : 472 - 493
  • [45] Quantitative model checking of linear-time properties based on generalized possibility measures
    Li, Yongming
    [J]. FUZZY SETS AND SYSTEMS, 2017, 320 : 17 - 39
  • [46] A LINEAR-TIME ALGORITHM TO COMPUTE A DOMINATING PATH IN AN AT-FREE GRAPH
    CORNEIL, DG
    OLARIU, S
    STEWART, L
    [J]. INFORMATION PROCESSING LETTERS, 1995, 54 (05) : 253 - 257
  • [47] Model checking memoryful linear-time logics over one-counter automata
    Demri, Stephane
    Lazic, Ranko
    Sangnier, Arnaud
    [J]. THEORETICAL COMPUTER SCIENCE, 2010, 411 (22-24) : 2298 - 2316
  • [48] Model Checking of Possibilistic Linear-Time Properties Based on Generalized Possibilistic Decision Processes
    Li, Yongming
    Liu, Wuniu
    Wang, Junmei
    Yu, Xianfeng
    Li, Chao
    [J]. IEEE TRANSACTIONS ON FUZZY SYSTEMS, 2023, 31 (10) : 3495 - 3506
  • [49] A linear-time algorithm for computing collision-free path on reconfigurable mesh
    Wang, Dajin
    [J]. PARALLEL COMPUTING, 2008, 34 (09) : 487 - 496
  • [50] A LINEAR-TIME ALGORITHM TO COMPUTE THE RELIABILITY OF PLANAR CUBE-FREE NETWORKS
    POLITOF, T
    SATYANARAYANA, A
    [J]. IEEE TRANSACTIONS ON RELIABILITY, 1990, 39 (05) : 557 - 563