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 条
  • [21] Model checking for real-time temporal, cooperation and epistemic properties
    Cao, Zining
    Intelligent Information Processing III, 2006, 228 : 63 - 72
  • [22] Model checking of real-time reachability properties using abstractions
    Daws, C
    Tripakis, S
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, 1998, 1384 : 313 - 329
  • [23] Dense time-based model-checking of real-time systems
    Zhang, GQ
    Rong, M
    PROCEEDINGS OF THE 11TH JOINT INTERNATIONAL COMPUTER CONFERENCE, 2005, : 785 - 788
  • [24] Verifying distributed real-time properties of embedded systems via graph transformations and model checking
    Gabor Madl
    Sherif Abdelwahed
    Douglas C. Schmidt
    Real-Time Systems, 2006, 33 : 77 - 100
  • [25] Verifying distributed real-time properties of embedded systems via graph transformations and model checking
    Gabor, MU
    Sherif, AU
    Schmidt, DC
    REAL-TIME SYSTEMS, 2006, 33 (1-3) : 77 - 100
  • [26] Model Checking Process Algebra of Communicating Resources for Real-time Systems
    Boudjadar, A. Jalil
    Kim, Jin Hyun
    Larsen, Kim G.
    Nyman, Ulrik
    2014 26TH EUROMICRO CONFERENCE ON REAL-TIME SYSTEMS (ECRTS 2014), 2014, : 51 - 60
  • [27] Probabilistic model checking: Formalisms and algorithms for discrete and real-time systems
    Courcoubetis, C
    Tripakis, S
    VERIFICATION OF DIGITAL AND HYBRID SYSTEM, 2000, 170 : 183 - 219
  • [28] Approximate Model Checking of Real-time Systems for Linear Duration Invariants
    Choe, Changil
    Han, Song
    Dang Van Hung
    2012 INTERNATIONAL CONFERENCE ON APPLIED INFORMATICS AND COMMUNICATION (ICAIC 2012), 2013, : 16 - 21
  • [29] Spatio-temporal model checking for mobile real-time systems
    Quesel, Jan-David
    Schaefer, Andreas
    THEORETICAL ASPECTS OF COMPUTING - ICTAC 2006, 2006, 4281 : 347 - 361
  • [30] Bounded model checking for GSMP models of stochastic real-time systems
    Alur, Rajeev
    Bernadsky, Mikhail
    HYBRID SYSTEMS: COMPUTATION AND CONTROL, PROCEEDINGS, 2006, 3927 : 19 - 33
12345