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 条

[41] High Fidelity Simulation of Hybrid Systems using Higher Order Hybrid Automata [J].

Ro, Jin Woo ;

Malik, Avinash ;

Roop, Partha .

IEEE TRANSACTIONS ON COMPUTERS, 2022, 71 (07) :1668-1680

[42] A Virtual Model of Manufacturing System Based on Hybrid Automata [J].

Jiang Danding ;

Zhou Jingtao ;

Zhao Ying ;

Li Enming .

ICCMA 2018: PROCEEDINGS OF THE 6TH INTERNATIONAL CONFERENCE ON CONTROL, MECHATRONICS AND AUTOMATION, 2018, :139-143

[43] Hybrid automata: an insight into the discrete abstraction of discontinuous systems [J].

Navarro-Lopez, Eva M. ;

Carter, Rebekah .

INTERNATIONAL JOURNAL OF SYSTEMS SCIENCE, 2011, 42 (11) :1883-1898

[44] Modelling of a virtual power plant using hybrid automata [J].

Javaid, Chaudhry Jibran ;

Allahham, Adib ;

Giaouris, Damian ;

Blake, Simon ;

Taylor, Phil .

JOURNAL OF ENGINEERING-JOE, 2019, (17) :3918-3922

[45] The Geometrical Criterion for Stability of Linear Hybrid Automata on the Plane [J].

Kuzmych, Olena ;

Aitouche, Abdelouhab ;

Shah, M. Zamurad .

2013 INTERNATIONAL CONFERENCE ON CONTROL, DECISION AND INFORMATION TECHNOLOGIES (CODIT), 2013, :118-123

[46] Computation of Lyapunov functions for hybrid automata via LMIs [J].

Masubuchi, I ;

Yabuki, S ;

Tsuji, T .

IEICE TRANSACTIONS ON FUNDAMENTALS OF ELECTRONICS COMMUNICATIONS AND COMPUTER SCIENCES, 2004, E87A (11) :2937-2943

[47] Synthesis of Parametric Hybrid Automata from Time Series [J].

Soto, Miriam Garcia ;

Henzinger, Thomas A. ;

Schilling, Christian .

AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, ATVA 2022, 2022, 13505 :337-353

[48] Modeling Bipedal Locomotion Trajectories Using Hybrid Automata [J].

Nandi, Gora Chand ;

Semwal, Vijay Bhaskar ;

Raj, Manish ;

Jindal, Akanksha .

PROCEEDINGS OF THE 2016 IEEE REGION 10 CONFERENCE (TENCON), 2016, :1013-1018

[49] Formalizing Metabolic-Regulatory Networks by Hybrid Automata [J].

Liu, Lin ;

Bockmayr, Alexander .

ACTA BIOTHEORETICA, 2020, 68 (01) :73-85

[50] Formalizing Metabolic-Regulatory Networks by Hybrid Automata [J].

Lin Liu ;

Alexander Bockmayr .

Acta Biotheoretica, 2020, 68 :73-85

← 1 2 3 4 5 →