Reachability verification for hybrid automata

被引：0

作者：

Henzinger, TA ^{[1
]}

Rusu, V

机构：

[1] Univ Calif Berkeley, Dept EECS, Berkeley, CA 94720 USA

[2] SRI Int, Comp Sci Lab, Menlo Park, CA 94025 USA

来源：

HYBRID SYSTEMS: COMPUTATION AND CONTROL | 1998年 / 1386卷

关键词：

hybrid automata; reachability verification; theorem proving;

D O I：

暂无

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

We study the reachability problem for hybrid automata. Automatic approaches, which attempt to construct the reachable region by symbolic execution, often do not terminate. In these cases, we require the user to guess the reachable region, and we use a theorem prover (Pvs) to verify the guess. We classify hybrid automata according to the theory in which their reachable region can be defined finitely. This is the theory in which the prover needs to operate in order to verify the guess. The approach is interesting, because an appropriate guess can often be deduced by extrapolating from the first few steps of symbolic execution.

引用

页码：190 / 204

页数：15

共 50 条

[21] Inclusion dynamics hybrid automata [J].

Casagrande, Alberto ;

Piazza, Carla ;

Policriti, Alberto ;

Mishra, Bud .

INFORMATION AND COMPUTATION, 2008, 206 (12) :1394-1424

[22] Discrete Semantics for Hybrid Automata [J].

Casagrande, Alberto ;

Piazza, Carla ;

Policriti, Alberto .

DISCRETE EVENT DYNAMIC SYSTEMS-THEORY AND APPLICATIONS, 2009, 19 (04) :471-493

[23] Diagnosis of Hybrid Dynamical Systems through Hybrid Automata [J].

Belkacem, L. ;

Mhamdi, L. ;

Simeu-Abazi, Z. ;

Messaoud, H. ;

Gascard, E. .

IFAC PAPERSONLINE, 2016, 49 (12) :990-995

[24] Superposition Principle in Composable Hybrid Automata [J].

Akhundov, Jafar ;

Troeger, Peter ;

Werner, Matthias .

FUNDAMENTA INFORMATICAE, 2018, 157 (04) :321-339

[25] Embeddings of hybrid automata in process algebra [J].

Willemse, TAC .

INTEGRATED FORMAL METHODS, PROCEEDINGS, 2004, 2999 :343-362

[26] New approach of diagnosis with hybrid automata [J].

Olfa, Azzabi ;

Ben Njima, Chakib ;

Messaoud, Hassani .

2017 INTERNATIONAL CONFERENCE ON CONTROL, AUTOMATION AND DIAGNOSIS (ICCAD), 2017, :298-302

[27] Some Problems of Analysis of Hybrid Automata [J].

Skobelev V.V. ;

Skobelev V.G. .

Skobelev, V.V., 2018, Springer Science and Business Media, LLC (54) :517-526

[28] A computable and compositional semantics for hybrid automata [J].

Bresolin, Davide ;

Collins, Pieter ;

Geretti, Luca ;

Segala, Roberto ;

Villa, Tiziano ;

Gonzalez, Sanja Zivanovic .

PROCEEDINGS OF THE 23RD INTERNATIONAL CONFERENCE ON HYBRID SYSTEMS: COMPUTATION AND CONTROL (HSCC2020) (PART OF CPS-IOT WEEK), 2020,

[29] Reachset Conformance Testing of Hybrid Automata [J].

Roehm, Hendrik ;

Oehlerking, Jens ;

Woehrle, Matthias ;

Althoff, Matthias .

HSCC'16: PROCEEDINGS OF THE 19TH INTERNATIONAL CONFERENCE ON HYBRID SYSTEMS: COMPUTATION AND CONTROL, 2016, :277-286

[30] On the formal verification of hybrid systems [J].

Guéguen, H ;

Zaytoon, J .

CONTROL ENGINEERING PRACTICE, 2004, 12 (10) :1253-1267

← 1 2 3 4 5 →