Model checking real-time properties of symmetric systems

被引：0
|
作者：
Emerson, EA [1 ]
Trefler, RJ
机构：
[1] Univ Texas, Dept Comp Sci, Austin, TX 78712 USA
[2] Univ Texas, Comp Engn Res Ctr, Austin, TX 78712 USA
来源：
MATHEMATICAL FOUNDATIONS OF COMPUTER SCIENCE 1998 | 1998年 / 1450卷
关键词：
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We develop efficient algorithms for model checking quantitative properties of symmetric reactive systems in the general framework of a Real-Time Mu-calculus. Previous work has been limited to qualitative correctness properties. Our work not only permits handling of quantitative correctness, but it provides a strictly more expressive framework for qualitative correctness since the Mu-calculus strictly subsumes, e.g, CTL*. Unlike the previous "group-theoretic" approaches of [CE96] and [ES96] and the technical "automata-theoretic" approach of [ES97], our new approach may be viewed as "model-theoretic".
引用
收藏
页码：427 / 436
页数：10
相关论文
共 50 条
  • [1] Compositional Model Checking for Real-Time Systems
    Hou, J.
    Li, X.
    Fan, X.
    Zheng, G.
    Software Engineering Notes, 23 (01):
  • [2] Symbolic model checking of real-time systems
    Logothetis, G
    Schneider, K
    EIGHTH INTERNATIONAL SYMPOSIUM ON TEMPORAL REPRESENTATION AND REASONING, PROCEEDINGS, 2001, : 214 - 223
  • [3] Local model checking for real-time systems
    Sokolsky, OV
    Smolka, SA
    COMPUTER AIDED VERIFICATION, 1995, 939 : 211 - 224
  • [4] SYMBOLIC MODEL CHECKING FOR REAL-TIME SYSTEMS
    HENZINGER, TA
    NICOLLIN, X
    SIFAKIS, J
    YOVINE, S
    INFORMATION AND COMPUTATION, 1994, 111 (02) : 193 - 244
  • [5] Symbolic model checking for discrete real-time systems
    Xiangyu LUO
    Lijun WU
    Qingliang CHEN
    Haibo LI
    Lixiao ZHENG
    Zuxi CHEN
    Science China(Information Sciences), 2018, 61 (05) : 203 - 225
  • [6] MODEL-CHECKING FOR PROBABILISTIC REAL-TIME SYSTEMS
    ALUR, R
    COURCOUBETIS, C
    DILL, D
    LECTURE NOTES IN COMPUTER SCIENCE, 1991, 510 : 115 - 126
  • [7] Symbolic model checking for discrete real-time systems
    Xiangyu Luo
    Lijun Wu
    Qingliang Chen
    Haibo Li
    Lixiao Zheng
    Zuxi Chen
    Science China Information Sciences, 2018, 61
  • [8] Model-checking real-time concurrent systems
    Romanovsky, I
    16TH ANNUAL INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING (ASE 2001), PROCEEDINGS, 2001, : 439 - 439
  • [9] Symbolic model checking for discrete real-time systems
    Luo, Xiangyu
    Wu, Lijun
    Chen, Qingliang
    Li, Haibo
    Zheng, Lixiao
    Chen, Zuxi
    SCIENCE CHINA-INFORMATION SCIENCES, 2018, 61 (05)
  • [10] On checking parallel real-time systems for linear duration properties
    Zhao, JH
    Hung, DV
    FORMAL TECHNIQUES IN REAL-TIME AND FAULT-TOLERANT SYSTEMS, 1998, 1486 : 241 - 250
12345