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 条

[31] Cancer hybrid automata: Model, beliefs and therapy [J].

Loohuis, Loes Olde ;

Witzel, Andreas ;

Mishra, Bud .

INFORMATION AND COMPUTATION, 2014, 236 :68-86

[32] Analysis of slope-parametric hybrid automata [J].

Boniol, F ;

Burgueno, A ;

Roux, O ;

Rusu, V .

HYBRID AND REAL-TIME SYSTEMS, 1997, 1201 :75-80

[33] Hybrid Automata as a Modelling Approach in the Behavioural Sciences [J].

Buntins, Matthias ;

Schicke, Jens-W. ;

Eggert, Frank ;

Goltz, Ursula .

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2013, 297 :47-59

[34] A Hybrid Automata model of social networking addiction [J].

Nasti, Lucia ;

Milazzo, Paolo .

JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, 2018, 100 :215-229

[35] On the issue of stability of hybrid automata by a part of variables [J].

Bychkov A.S. ;

Suprun O.N. ;

Krzhyzh I. ;

Navotna V. .

Journal of Automation and Information Sciences, 2019, 51 (10) :23-30

[36] Languages and models for hybrid automata: A coalgebraic perspective [J].

Neves, Renato ;

Barbosa, Luis S. .

THEORETICAL COMPUTER SCIENCE, 2018, 744 :113-142

[37] Modeling a system with hybrid automata and multi -models [J].

Azzabi, Olfa ;

Ben Njima, Chakib ;

Messaoud, Hassani .

2017 INTERNATIONAL CONFERENCE ON CONTROL, AUTOMATION AND DIAGNOSIS (ICCAD), 2017, :87-90

[38] A PRECISION IRRIGATION MODEL USING HYBRID AUTOMATA [J].

Lozoya, C. ;

Favela-Contreras, A. ;

Aguilar-Gonzalez, A. ;

Orona, L. .

TRANSACTIONS OF THE ASABE, 2019, 62 (06) :1639-1650

[39] Automatic Synthesis of Switching Controllers for Linear Hybrid Systems: Reachability Control [J].

Benerecetti, Massimo ;

Faella, Marco .

ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS, 2017, 16 (04)

[40] From Hybrid Data-Flow Languages to Hybrid Automata: A Complete Translation [J].

Schrammel, Peter ;

Jeannet, Bertrand .

HSCC 12: PROCEEDINGS OF THE 15TH ACM INTERNATIONAL CONFERENCE ON HYBRID SYSTEMS: COMPUTATION AND CONTROL, 2012, :167-176

← 1 2 3 4 5 →