Data-structures for the verification of timed automata

被引：0
|
作者：
Asarin, E
Bozga, M
Kerbrat, A
Maler, O
Pnueli, A
Rasse, A
机构：
[1] Verimag, Ctr Equat, F-38610 Gieres, France
[2] Weizmann Inst Sci, Dept Comp Sci, IL-76100 Rehovot, Israel
[3] Russian Acad Sci, Inst Informat Transmiss Problems, Moscow 101447, Russia
来源：
HYBRID AND REAL-TIME SYSTEMS | 1997年 / 1201卷
关键词：
D O I：
暂无
中图分类号：
TP39 [计算机的应用];
学科分类号：
081203 ; 0835 ;
摘要：
In this paper we suggest numerical decision diagrams, a BDD- based data-structure for representing certain subsets of the Euclidean space, namely those encountered in verification of timed automata. Unlike other representation schemes, NDD's are canonical and provide for all the necessary operations needed in the verification and synthesis of timed automata. We report some preliminary experimental results.
引用
收藏
页码：346 / 360
页数：15
相关论文
共 50 条
  • [1] Efficient verification of timed automata with BDD-like data-structures
    Wang, F
    [J]. VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, 2003, 2575 : 189 - 205
  • [2] VERIFICATION FOR TIMED AUTOMATA EXTENDED WITH UNBOUNDED DISCRETE DATA STRUCTURES
    Quaas, Karin
    [J]. LOGICAL METHODS IN COMPUTER SCIENCE, 2015, 11 (03)
  • [3] Efficient verification of timed automata with BDD-like data structures
    Wang F.
    [J]. International Journal on Software Tools for Technology Transfer, 2004, 6 (1) : 77 - 97
  • [4] Dynamic data structures for timed automata acceptance
    Grez, Alejandro
    Mazowiecki, Filip
    Pilipczuk, Michal
    Puppis, Gabriele
    Riveros, Cristian
    [J]. Leibniz International Proceedings in Informatics, LIPIcs, 2021, 214
  • [5] Dynamic Data Structures for Timed Automata Acceptance
    Grez, Alejandro
    Mazowiecki, Filip
    Pilipczuk, Michal
    Puppis, Gabriele
    Riveros, Cristian
    [J]. ALGORITHMICA, 2022, 84 (11) : 3223 - 3245
  • [6] Dynamic Data Structures for Timed Automata Acceptance
    Alejandro Grez
    Filip Mazowiecki
    Michał Pilipczuk
    Gabriele Puppis
    Cristian Riveros
    [J]. Algorithmica, 2022, 84 : 3223 - 3245
  • [7] A temporal approach to specification and verification of pointer data-structures
    Kubica, M
    [J]. FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, PROCEEDINGS, 2003, 2621 : 231 - 245
  • [8] Reachability results for timed automata with unbounded data structures
    Ruggero Lanotte
    Andrea Maggiolo-Schettini
    Angelo Troina
    [J]. Acta Informatica, 2010, 47 : 279 - 311
  • [9] Reachability results for timed automata with unbounded data structures
    Lanotte, Ruggero
    Maggiolo-Schettini, Andrea
    Troina, Angelo
    [J]. ACTA INFORMATICA, 2010, 47 (5-6) : 279 - 311
  • [10] Unification & sharing in timed automata verification
    David, A
    Behrmann, G
    Larsen, KG
    Yi, W
    [J]. MODEL CHECKING SOFTWARE, 2003, 2648 : 225 - 229
12345