Model Checking MASL Specification of Distributed Real-Time Systems

被引：0
|
作者：
Bugaichenko, D. Yu.
机构：
来源：
VESTNIK ST PETERSBURG UNIVERSITY-MATHEMATICS | 2007年 / 40卷 / 03期
关键词：
D O I：
10.3103/S1063454107030065
中图分类号：
O1 [数学];
学科分类号：
0701 ; 070101 ;
摘要：
We present model checking algorithms for MASL specification of distributed real-time systems. The proposed algorithms use symbolic model checking approach by analogy with model checking algorithms for branching-time temporal logic CTL and alternating-time temporal logic ATL. For the fixed environment case, the algorithm is polynomial-time in the specification length and sizes of the sets of system states and actions. For the dynamic environment case, the algorithm is polynomial-time in the model size, but it is exponential-time in the structure of environment specification.
引用
收藏
页码：201 / 208
页数：8
相关论文
共 50 条
  • [1] MASL: A logic for the specification of multiagent real-time systems
    Bugaychenko, Dmitry
    Soloviev, Igor
    [J]. MULTI-AGENT SYSTEMS AND APPLICATIONS V, PROCEEDINGS, 2007, 4696 : 183 - 192
  • [2] Statistical Model Checking of Distributed Real-Time Actor Systems
    Nigro, Libero
    Sciammarella, Paolo F.
    [J]. 2017 IEEE/ACM 21ST INTERNATIONAL SYMPOSIUM ON DISTRIBUTED SIMULATION AND REAL TIME APPLICATIONS (DS-RT), 2017, : 188 - 195
  • [3] Scheduling distributed real-time systems by satisfiability checking
    Metzner, A
    Fränzle, M
    Herde, C
    Stierand, I
    [J]. 11th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications, Proceedings, 2005, : 409 - 415
  • [4] Specification and modeling of dynamic, distributed real-time systems
    Welch, LR
    Ravindran, B
    Shirazi, BA
    Bruggeman, C
    [J]. 19TH IEEE REAL-TIME SYSTEMS SYMPOSIUM, PROCEEDINGS, 1998, : 72 - 81
  • [5] COMPOSITIONAL PRIORITY SPECIFICATION IN REAL-TIME DISTRIBUTED SYSTEMS
    SHYAMASUNDAR, RK
    LIU, LY
    [J]. SADHANA-ACADEMY PROCEEDINGS IN ENGINEERING SCIENCES, 1992, 17 : 75 - 93
  • [6] Symbolic model checking of real-time systems
    Logothetis, G
    Schneider, K
    [J]. EIGHTH INTERNATIONAL SYMPOSIUM ON TEMPORAL REPRESENTATION AND REASONING, PROCEEDINGS, 2001, : 214 - 223
  • [7] Local model checking for real-time systems
    Sokolsky, OV
    Smolka, SA
    [J]. COMPUTER AIDED VERIFICATION, 1995, 939 : 211 - 224
  • [8] SYMBOLIC MODEL CHECKING FOR REAL-TIME SYSTEMS
    HENZINGER, TA
    NICOLLIN, X
    SIFAKIS, J
    YOVINE, S
    [J]. INFORMATION AND COMPUTATION, 1994, 111 (02) : 193 - 244
  • [9] Requirement specification and model-checking of a real-time scheduler implementation
    Boukir, Khaoula
    Bechennec, Jean-Luc
    Deplanche, Anne-Marie
    [J]. 28TH INTERNATIONAL CONFERENCE ON REAL TIME NETWORKS AND SYSTEMS, RTNS 2020, 2020, : 89 - 99
  • [10] A framework for the specification of test cases for real-time distributed systems
    Walter, T
    Grabowski, J
    [J]. INFORMATION AND SOFTWARE TECHNOLOGY, 1999, 41 (11-12) : 781 - 798
12345