Symbolic model checking for simply-timed systems

被引：0
|
作者：
Markey, N
Schnoebelen, P
机构：
[1] Free Univ Brussels, Dept Informat, Brussels, Belgium
[2] ENS Cachan, Lab Specificat & Verificat, Cachan, France
[3] CNRS, UMR 8643, Cachan, France
来源：
FORMAL TECHNIQUES, MODELLING AND ANALYSIS OF TIMED AND FAULT-TOLERANT SYSTEMS, PROCEEDINGS | 2004年 / 3253卷
关键词：
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We describe OBDD-based symbolic model checking algorithms for simply-timed systems, i.e. finite state graphs where transitions carry a duration. These durations can be arbitrary natural numbers. A simple and natural semantics for these systems opens the way for improved efficiency. Our algorithms have been implemented in NuSMV and perform well in practice (on standard case studies).
引用
收藏
页码：102 / 117
页数：16
相关论文
共 50 条
  • [31] Hybrid multiagent systems with timed synchronization - Specification and model checking
    Furbach, Ulrich
    Murray, Jan
    Schmidsberger, Falk
    Stolzenburg, Frieder
    PROGRAMMING MULTI-AGENT SYSTEMS, 2008, 4908 : 205 - +
  • [32] Simple Bounded MTLK Model Checking for Timed Interpreted Systems
    Zbrzezny, Agnieszka M.
    Zbrzezny, Andrzej
    AGENT AND MULTI-AGENT SYSTEMS: TECHNOLOGY AND APPLICATIONS, 2018, 74 : 88 - 98
  • [33] Efficient timed model checking for discrete-time systems
    Laroussinie, F
    Markey, N
    Schnoebelen, P
    THEORETICAL COMPUTER SCIENCE, 2006, 353 (1-3) : 249 - 271
  • [34] Symbolic model checking
    McMillan, KL
    VERIFICATION OF DIGITAL AND HYBRID SYSTEM, 2000, 170 : 117 - 137
  • [35] Synchronous closing and flow analysis for model checking timed systems
    Ioustinova, N
    Sidorova, N
    Steffen, M
    FORMAL METHODS FOR COMPONENTS AND OBJECTS, 2003, 3188 : 292 - 313
  • [36] Model Checking Timed Hyperproperties in Discrete-Time Systems
    Bonakdarpour, Borzoo
    Prabhakar, Pavithra
    Sanchez, Cesar
    NASA FORMAL METHODS (NFM 2020), 2020, 12229 : 311 - 328
  • [37] Symbolic systems, explicit properties: On hybrid approaches for LTL symbolic model checking
    Sebastiani R.
    Tonetta S.
    Vardi M.Y.
    International Journal on Software Tools for Technology Transfer, 2011, 13 (4) : 319 - 335
  • [38] Symbolic systems, explicit properties: On hybrid approaches for LTL symbolic model checking
    Sebastiani, R
    Tonetta, S
    Vardi, MY
    COMPUTER AIDED VERIFICATION, PROCEEDINGS, 2005, 3576 : 350 - 363
  • [39] Model checking for timed statecharts
    Qian, JY
    Xu, BW
    FORMAL TECHNIQUES FOR NETWORKED AND DISTRIBUTED SYSTEMS - FORTE 2005, 2005, 3731 : 261 - 274
  • [40] Parametric Timed Model Checking for Guaranteeing Timed Opacity
    Andre, Etienne
    Sun, Jun
    AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS (ATVA 2019), 2019, 11781 : 115 - 130
12345