Better abstractions for timed automata

被引：20

作者：

Herbreteau, Frederic ^{[1
]}

Srivathsan, B. ^{[2
]}

Walukiewicz, Igor ^{[1
]}

机构：

[1] Univ Bordeaux, Bordeaux INP, CNRS, LaBRI,UMR 5800, Talence, France

[2] Chennai Math Inst, Madras, Tamil Nadu, India

来源：

INFORMATION AND COMPUTATION | 2016年 / 251卷

关键词：

Timed automata; Reachability problem; Non-convex abstractions; SYSTEMS; REACHABILITY; ALGORITHM; CHECKING;

D O I：

10.1016/j.ic.2016.07.004

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

We study the Teachability problem for timed automata. A standard solution to this problem involves computing a search tree whose nodes are abstractions of zones. These abstractions preserve underlying simulation relations on the state space of the automaton. For both effectiveness and efficiency reasons, they are parameterized by the maximal lower and upper bounds (LU-bounds) occurring in the guards of the automaton. One such abstraction is the a <= Lu abstraction defined by Behrmann et al. Since this abstraction can potentially yield non-convex sets, it has not been used in implementations. Firstly, we prove that a <= LU abstraction is the coarsest abstraction with respect to LU-bounds that is sound and complete for reachability. Secondly, we provide an efficient technique to use the a <= Lu abstraction to solve the reachability problem. (C) 2016 Elsevier Inc. All rights reserved.

引用

页码：67 / 90

页数：24

共 26 条

[1] A THEORY OF TIMED AUTOMATA [J].

ALUR, R ;

DILL, DL .

THEORETICAL COMPUTER SCIENCE, 1994, 126 (02) :183-235

[2]

ALUR R, 1992, LECT NOTES COMPUT SC, V630, P340

[3] Lower and upper bounds in zone-based abstractions of timed automata [J].

Gerd Behrmann ;

Patricia Bouyer ;

Kim G. Larsen ;

Radek Pelánek .

International Journal on Software Tools for Technology Transfer, 2006, 8 (3) :204-215

[4]

Behrmann G, 2003, LECT NOTES COMPUT SC, V2619, P254

[5]

Behrmann G, 2006, INT CONF QUANT EVAL, P125

[6] Timed automata: Semantics, algorithms and tools [J].

Bengtsson, J ;

Yi, W .

LECTURES ON CONCURRENCY AND PETRI NETS: ADVANCES IN PETRI NETS, 2004, 3098 :87-124

[7]

Berthomieu B., 1983, Information Processing 83. Proceedings of the IFIP 9th World Computer Congress, P41

[8] Forward analysis of updatable timed automata [J].

Bouyer, P .

FORMAL METHODS IN SYSTEM DESIGN, 2004, 24 (03) :281-320

[9]

Bouyer P., 2009, MEMOIRE HABILITATION

[10] Symbolic Optimal Reachability in Weighted Timed Automata [J].

Bouyer, Patricia ;

Colange, Maximilien ;

Markey, Nicolas .

COMPUTER AIDED VERIFICATION, (CAV 2016), PT I, 2016, 9779 :513-530

← 1 2 3 →