How to Capture Hybrid Systems Evolution into Slices of Parallel Hyperplanes

0333950 - ÚI 2010 RIV ES eng C - Konferenční příspěvek (zahraniční konf.)
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]
Grant CEP: GA ČR GC201/08/J020; GA ČR GD201/09/H057
Výzkumný záměr: CEZ:AV0Z10300504
Klíčová slova: verification * hybrid systems * timed automata
Kód oboru RIV: IN - Informatika

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é.
Trvalý link: http://hdl.handle.net/11104/0178807