How to Capture Hybrid Systems Evolution into Slices of Parallel Hyperplanes

0333950 - ÚI 2010 RIV ES eng C - Conference Paper (international conference)
Dzetkulič, Tomáš - Ratschan, Stefan
How to Capture Hybrid Systems Evolution into Slices of Parallel Hyperplanes.
[Jak zachytit evoluci hybridních systémů do řezů paralelních hyper-rovnic.]
ADHS'09. Preprints of the 3rd IFAC Conference on Analysis and Design of Hybrid Systems. Zaragoza: Universidad de Zaragoza, 2009 - (Giua, A.; Mahulea, C.; Silva, M.; Zaytoon, J.), s. 274-279
[ADHS'09. IFAC Conference on Analysis and Design of Hybrid Systems /3./. Zaragoza (ES), 16.09.2009-18.09.2009]
R&D Projects: GA ČR GC201/08/J020; GA ČR GD201/09/H057
Institutional research plan: CEZ:AV0Z10300504
Keywords : verification * hybrid systems * timed automata
Subject RIV: IN - Informatics, Computer Science

In this paper we make a step towards an algorithm for the verification of hybrid systems that, on the one hand allows very general inputs (e.g., with non-linear ordinary differential equations), but on the other hand exploits the structure of those parts of the input that represent special cases (e.g., clocks). We show how to compute slices of parallel hyperplanes separating reachable from unreachable parts of the state space for a given abstraction of the input system, and demonstrate the usefulness of such slices within an abstraction refinement algorithm based on hyper-rectangles.

V tomto článku uděláme jeden krok k algoritmu pro verifikaci hybridních systémů, který na jedné straně dovoluje velmi široké vstupy, ale na druhé straně využívá strukturu těch částí vstupů které reprezentují zvláštní případy. Naše metoda počítá řez paralelních hyper-rovin, které oddělují dosažitelnou část stavového prostoru od nedosažitelné.
Permanent Link: http://hdl.handle.net/11104/0178807