Better abstractions for timed automata

被引：19

作者：

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

共 50 条

[1] Better Abstractions for Timed Automata
Herbreteau, Frederic
Srivathsan, B.
Walukiewicz, Igor
2012 27TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS), 2012, : 375 - 384
[2] Approximate timed abstractions of hybrid automata
D'Innocenzo, A.
Julius, A. A.
Di Benedetto, M. D.
Pappas, G. J.
PROCEEDINGS OF THE 46TH IEEE CONFERENCE ON DECISION AND CONTROL, VOLS 1-14, 2007, : 4362 - +
[3] Complete abstractions of dynamical systems by timed automata
Sloth, Christoffer
Wisniewski, Rafael
NONLINEAR ANALYSIS-HYBRID SYSTEMS, 2013, 7 (01) : 80 - 100
[4] Reductions and Abstractions for Optimization of Modular Timed Automata
Lennartson, Bengt
IFAC PAPERSONLINE, 2022, 55 (28): : 344 - 349
[5] Lower and upper bounds in zone based abstractions of timed automata
Behrmann, G
Bouyer, P
Larsen, KG
Pelánek, R
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2004, 2988 : 312 - 326
[6] Parameter synthesis for probabilistic timed automata using stochastic game abstractions
Jovanovic, Aleksandra
Kwiatkowska, Marta
THEORETICAL COMPUTER SCIENCE, 2018, 735 : 64 - 81
[7] Lower and upper bounds in zone-based abstractions of timed automata
Gerd Behrmann
Patricia Bouyer
Kim G. Larsen
Radek Pelánek
International Journal on Software Tools for Technology Transfer, 2006, 8 (3) : 204 - 215
[8] Checking Timed Buchi Automata Emptiness Using LU-Abstractions
Li, Guangyuan
FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS, PROCEEDINGS, 2009, 5813 : 228 - 242
[9] Nonblocking Supervisory Control Synthesis of Timed Automata using Abstractions and Forcible Events
Rashidinejad, Aida
van der Graaf, Patrick
Reniers, Michel
16TH IEEE INTERNATIONAL CONFERENCE ON CONTROL, AUTOMATION, ROBOTICS AND VISION (ICARCV 2020), 2020, : 1033 - 1040
[10] Generation of safe operation sequences using iterative refinements and abstractions of timed automata
Cochard, Thomas
Gouyon, David
Petin, Jean-Francois
2016 IEEE 21ST INTERNATIONAL CONFERENCE ON EMERGING TECHNOLOGIES AND FACTORY AUTOMATION (ETFA), 2016,

← 1 2 3 4 5 →