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 DESIGN | 1993年 / 2卷 / 02期
关键词：
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 条
  • [1] 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
  • [2] Efficient on-the-fly model-checking for regular alternation-free mu-calculus
    Mateescu, R
    Sighireanu, M
    [J]. SCIENCE OF COMPUTER PROGRAMMING, 2003, 46 (03) : 255 - 281
  • [3] Alternation-free modal mu-calculus for data trees (Extended abstract)
    Jurdzinski, Marcin
    Lazic, Ranko
    [J]. 22ND ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2007, : 131 - +
  • [4] Alternation-Free Weighted Mu-Calculus: Decidability and Completeness
    Larsen, Kim G.
    Mardare, Radu
    Xue, Bingtian
    [J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2015, 319 : 289 - 313
  • [5] Local model-checking of modal Mu-calculus on acyclic Labeled Transition Systems
    Mateescu, R
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANAYLSIS OF SYSTEMS, PROCEEDINGS, 2002, 2280 : 281 - 295
  • [6] LOCAL MODEL CHECKING IN THE MODAL MU-CALCULUS
    STIRLING, C
    WALKER, D
    [J]. THEORETICAL COMPUTER SCIENCE, 1991, 89 (01) : 161 - 177
  • [7] LOCAL MODEL CHECKING IN THE MODAL MU-CALCULUS
    STIRLING, C
    WALKER, D
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1989, 351 : 369 - 383
  • [8] Model-Checking the Higher-DimensionalModal mu-calculus
    Lange, Martin
    Lozes, Etienne
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2012, (77): : 39 - 46
  • [9] Local parallel model checking for the alternation-free μ-calculus
    Bollig, B
    Leucker, M
    Weber, M
    [J]. MODEL CHECKING SOFTWARE, PROCEEDINGS, 2002, 2318 : 128 - 147
  • [10] Simplifying the modal mu-calculus alternation hierarchy
    Bradfield, JC
    [J]. STACS 98 - 15TH ANNUAL SYMPOSIUM ON THEORETICAL ASPECTS OF COMPUTER SCIENCE, 1998, 1373 : 39 - 49
12345