Bounded Model Checking for Parametric Timed Automata

被引：0
|
作者：
Knapik, Michal [1 ]
Penczek, Wojciech [1 ,2 ]
机构：
[1] Polish Acad Sci, Inst Comp Sci, PL-01237 Warsaw, Poland
[2] Univ Nat Sci & Humanities, Inst Informat, PL-08110 Siedlce, Poland
来源：
TRANSACTIONS ON PETRI NETS AND OTHER MODELS OF CONCURRENCY V | 2012年 / 6900卷
关键词：
REACHABILITY; FRAGMENT; TOOL;
D O I：
暂无
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
This paper shows how bounded model checking can be applied to parameter synthesis for parametric timed automata with continuous time. While it is known that the general problem is undecidable even for reachability, we show how to synthesize a part of the set of all the parameter valuations under which the given property holds in a model. The results form a full theory which can be easily applied to parametric verification of a wide range of temporal formulae - we present such an implementation for the existential part of CTL-X.
引用
收藏
页码：141 / 159
页数：19
相关论文
共 50 条
  • [1] Improved Bounded Model Checking of Timed Automata
    Smith, Robert L.
    Bersani, Marcello M.
    Rossi, Matteo
    San Pietro, Pierluigi
    2021 IEEE/ACM 9TH INTERNATIONAL CONFERENCE ON FORMAL METHODS IN SOFTWARE ENGINEERING (FORMALISE 2021), 2021, : 97 - 110
  • [2] Linear parametric model checking of timed automata
    Hune, T
    Romijn, J
    Stoelinga, M
    Vaandrager, F
    JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING, 2002, 52-3 : 183 - 220
  • [3] Bounded Model Checking of an MITL Fragment for Timed Automata
    Kindermann, Roland
    Junttila, Tommi
    Niemela, Ilkka
    2013 13TH INTERNATIONAL CONFERENCE ON APPLICATION OF CONCURRENCY TO SYSTEM DESIGN (ACSD 2013), 2013, : 216 - 225
  • [4] Efficient encoding for bounded model checking of timed automata
    Chen, Zuxi
    Xu, Zhongwei
    Du, Junwei
    Mei, Meng
    Guo, Jing
    IEEJ TRANSACTIONS ON ELECTRICAL AND ELECTRONIC ENGINEERING, 2017, 12 (05) : 710 - 720
  • [5] Durations and parametric model-checking in timed automata
    Bruyere, Veronique
    Dall'olio, Emmanuel
    Raskin, Jean-Francois
    ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2008, 9 (02)
  • [6] Checking MTL Properties of Discrete Timed Automata via Bounded Model Checking
    Wozna-Szczesniak, Bozena
    Zbrzezny, Andrzej
    FUNDAMENTA INFORMATICAE, 2014, 135 (04) : 553 - 568
  • [7] Checking ACTL* properties of discrete timed automata via bounded model checking
    Wozna, B
    Zbrzezny, A
    FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS, 2003, 2791 : 18 - 33
  • [8] Optimized Step Semantics Encoding for Bounded Model Checking of Timed Automata
    Chen, Zuxi
    Fang, Huixing
    Luo, Xiangyu
    2019 13TH INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING (TASE 2019), 2019, : 93 - 98
  • [9] Durations, parametric model-checking in timed automata with Presburger arithmetic
    Bruyère, V
    Dall'Olio, E
    Raskin, JF
    STACS 2003, PROCEEDINGS, 2003, 2607 : 687 - 698
  • [10] SAT Based Bounded Model Checking with Partial Order Semantics for Timed Automata
    Malinowski, Janusz
    Niebert, Peter
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2010, 6015 : 405 - 419
12345