IV120 Spojité a hybridní systémy
Hybridní systémy - pokr.
David Šafránek
Jiří Barnat Jana Fabriková
Tento projekt je spolufinancován Evropským sociálním fondem a státním rozpočtem České republiky. NVESTICE DO ROZVOJE VZDĚLÁVÁNÍ
Modelovaní hybridních systémů
Pozorování
» Hybridní automaty slouží pro teoretický popis reálného hybridního systému.
• Díky abstrakci a zjednodušování, je možné specifikovat nereálné situace.
Rizika modelování
• Lze vytvořit systém, který nemá řešení.
• Lze vytvořit systém, který jehož řešení nejsou reálná.
• Lze vytvořit systém, který má nejednoznačná řešení.
Terminologie
• O systému, který nemá řešení (neexistuje běh systému) říkáme, že je blokující.
IV120 Hybridní systémy - pokr.
str. 2/35
Reálnost běhů
Pozorování
• Neblokující systém negarantuje, že řešení jsou reálná.
» Neblokující systém neimplikuje časově nekonečná chování.
Nereálná chování
• Běhy, ve kterých se provede nekonečně mnoho diskrétních přechodů v konečném čase - tzv. ZENO běhy.
• Vznikají abstrakcí a zjednodušováním. Diskuze
• Proč míček neskáče donekonečna?
• Je důležité pochopit abstrakce reálného světa, které mohou vést k ZENO chování.
IV120 Hybridní systémy - pokr.
str. 3/35
Nedeterminismus
Nedeterminismus
• Obecně lze charakterizovat jako absenci unikátního řešení, tj hybridní automat akceptuje více různých exekucí projeden iniciální stav.
• Při omezení na Lipschitz spojité funkce, které mají unikátní řešení, může být důvodem k nedeterminismu diskrétní složka.
Úmyslný nedeterminismus
• Může být použit pro modelování nejistoty.
• Je důležité umět rozlišit úmyslné použití nedeterminismu od neúmyslného.
Pozorování
• Nedeterminismus přináší problémy při analýze chování hybridních systémů i při syntéze kontrolérů.
IV120 Hybridní systémy - pokr.
str. 4/35
Problémy simulace/analýzy hybridních systémů
Existence řešení
• Jak detekovat existenci běhu (neblokujícnost)?
• Jak detekovat ZENO chování?
Unikátnost
• Jak simulovat nedeterminismus?
o Diskrétní přechod vs spojitá evoluce. • Diskrétní přechod vs diskrétní přechod.
• As-soon-as sémantika.
Nespojitost
• Jak detekovat splnitelnost stráží přechodů?
• Invariant stavu končí otevřeným intervalem [a, b) a následný přechod probíhá v čase [b].
Kompozicionalita
• Jak komponovat systém složené z hybridních komponent?
IV120 Hybridní systémy - pokr.
str. 5/35
Neblokující a deterministický hybridní automat
Neblokující hybridní automat
• Hybridní automat H se nazývá neblokující, pokud pro všechny iniciální stavy (q,x) G Init existuje nekonečný běh začínající v (q,x).
Deterministický hybridní automat
» Hybridní automat H se nazývá deterministický, pokud pro všechny iniciální stavy (q,x) G Init existuje nejvýše jeden maximální běh začínající v (q,x).
IV120 Hybridní systémy - pokr.
Príklad
Pozorování
• Následující automat je blokující a nedeterministický.
IV120 Hybridní systémy - pokr.
str. 7/35
Množina dosažitelných stavů
Definice dosažitelnosti
• Stav (q,x) G Q x X hybridního automatu H se nazýva dosažitelný, pokud existuje konečný běh (r, q, x), která končí v (q,x), tj. r = {[r/.r/]}^, /V < oo a (q/v(r^),xw(t£)) = (q,x).
Množina dosažitelných stavů
• Množinu dosažitelných stavů hybridního automatu H značíme /?eac/j, /?eac/? C Q x X.
• Fundamentální problém v oblasti hybridních systémů je výpočet množiny Reach pro zadaný hybridní automat.
Cvičení
» Zdůvodněte, proč Init C Reach.
IV120 Hybridní systémy - pokr.
str. 8/35
Množina tranzitních stavů
Neformálně
• Množina stavů H, ze kterých není možný spojitý vývoj.
Předpoklady
• Pro (q,x) G Q x X a nějaké e > 0 uvažme řešení x(-) : [0,e) —> R" následující diferenciální rovnice:
dx
= f {q, x), kde x(0) = x
• Za předpokladu Lipschitz spojitosti v x, řešení výše uvedené rovnice existuje a je unikátni.
Definice
• Trans = {(q, x) G Q x X \ Ve > 0 3ŕ G [0, e) takové, že (q,x(t)) ČDom(q)}.
IV120 Hybridní systémy - pokr.
str. 9/35
Spodní odhad množiny tranzitních stavů
Pozorování 1
• Spojitá evoluce nemůže probíhat mimo invariant (doménu) stavu.
• Tedy pro každý diskrétní stav q G Q, komplement domény stavu q, značený jako Dom(q)c musí být součástí množiny Trans.
{q} x Dom(q)c C Trans
qeQ
Pozorování 2
• Může Trans obsahovat i nějaké části z {q} x Dom(q)?
• Ano, pokud je doména uzavřená množina (obsahuje své hranice), části této hranice mohou být součástí Trans.
IV120 Hybridní systémy - pokr.
str. 10/35
Řešený příklad - Vodní nádrže
• Init = {qi, q2} x {x G R x R | x\ > r\ A x2 > r2J
• Dom(qi) = {x G R x R | x2 > r2J Dom(q2) = {x G R x R | xi > ri}
• E = {(qi,q2),(q2,qi)}
• G(q1, q2) = {x G R x R | x2 < r2} G(q2,qi) = {x G R x R | xi < ri}
• R{qi,q2,x) = R{q2,qi,x) = {x}
IV120 Hybridní systémy - pokr.
str. 11/35
Řešený příklad - Vodní nádrže
Příklad
• Předpokládejme, že 0 < v\, v2 < w. Spočítejte množinu Reach a množinu Trans.
Náznak řešení
• Reach obsahuje iniciální stavy:
Reach D {q1: q2} x {x G R2 | (xi > r{) A (x2 > r2)}
• Může Reach obsahovat i jiné stavy? Indukcí vzhledem k délce hybridní časové řady hypotetického běhu ukážeme, že ne.
Reach C {q1} q2} x {x G R2 | (xi > r\) A (x2 > r2)}.
• Uvážením obou inkluzí dostáváme, že
Reach = {q1, q2} x {x G R2 | (xi > r{) A (x2 > r2)}
IV120 Hybridní systémy - pokr. str. 12/35
Důkaz matematickou indukcí k délce běhu
Myšlenka použití indukce
• Indukce zahrnuje argumentaci pro spojitý vývoj času v rámci intervalu, a demonstraci, že po provedení diskrétního přechodu, invariant indukce platí.
Indukce
• Mějme běh (r, q,x). Jestliže r' Ľ r a tvrzení platí pro běh (t', q,x) pak platí i pro běh (r, q,x).
• BÁZE:
• Reach C /n/ŕ
• INDUKČNÍ KROK:
• Diskuze spojité evoluce.
• Diskuze diskrétního přechodu.
IV120 Hybridní systémy - pokr.
Řešený příklad - Vodní nádrže
Pozorování 1
• Spojitá evoluce není možná pokud
q = qi a X2 < r2, nebo q = q2 a x\ < r\
• tudíž
Trans D ({gi}x{x G R2 | x2 < r2})U({g2}x{x G R2 | x1 < ri}).
» Naopak víme, že spojitá evoluce je možná, pokud q = gi a x2 > r2, nebo q = g2 a *i > 1
• což dává
Trans C ({gi}x{x G R2 | x2 < r2})U({g2}x{x G R2 | xi < ri}). Krajní případy
• Pokud například q = q\ a x2 = r2. Plynutím času v qi by x2 kleslo pod r2, což je mimo doménu stavu. Tudíž hraniční hodnoty jsou v tomto případě součástí Trans.
Trans = ({gi}x{x G R2 | x2 < r2})U({g2}x{x G R2 | x1 < ri})
IV120 Hybridní systémy - pokr. str. 14/35
Cvičení
Úkol
• Zkuste odvodit, nebo alespoň ohraničit množiny Reach a Trans pro ostatní hybridní systémy definované v rámci minulé přednášky.
IV120 Hybridní systémy - pokr.
str. 15/35
Podmínka neblokujícnosti
Pozorování
• Hybridní automat je neblokující pokud pro všechny dosažitelné stavy, ve kterých není možná spojitá evoluce, je možné provést diskrétní přechod.
Lemma 1
• Hybridní automat H je neblokující, pokud pro všechny (q,x) G Reach n Trans existuje q' G Q takové, že (q, q') G E a x G G(q,q'). Pokud H je deterministický, pak je neblokující tehdy a jen tehdy, platí-li uvedená podmínka.
IV120 Hybridní systémy - pokr.
str. 16/35
Podmínka determinističnosti
Neformálně
• Automat je nedeterministický, pokud existuje dosažitelný stav, ze kterého se může realizovat alespoň jeden diskrétní přechod a zároveň z tohoto stavu může probíhat spojitá evoluce, anebo se mohou realizovat alespoň dva diskrétní přechody vedoucí do jiných diskrétních stavů.
Lemma 2
• Hybridní automat H je deterministický tehdy a jen tehdy, pokud pro všechny stavy (q,x) G Reach platí:
O pokud x e G(q, q') pro nějakou (q, q') e E, pak (q, x) e Trans O pokud (q, q') e E a (q, q") e £ takové, že q' ^ q", pak
x i G(q,q')nG(q,q") Q pokud (q, q') e E a x e G(q, q'), pak R(q, q', x) = {x'}. ťJ
množina obsahuje právě jeden konkrétní prvek.
IV120 Hybridní systémy - pokr.
str. 17/35
Využití Lemmat 1 a 2
Tvrzení
• Hybridní automat akceptuje unikátni nekonečný běh pro každý iniciální stav, pokud splňuje podmínky Lemat 1 a 2.
Poznámka
• Lemata se vyjadřují o vlastnostech stavů v množině Reach. Pokud nás však zajímá existence a unikátnost běhů pouze z počátečních podmínek, je možné formulovaná lemata rozšířit na všechny možné stavy (i nedosažitelné) a tím se vyhnout náročnému výpočtu množiny Reach.
IV120 Hybridní systémy - pokr.
str. 18/35
Príklad
Úkol
• Analyzujte platnost podmínek uvedených lemat na příkladu s vodními nádržemi za předpokladu 0 < v\, V2 < w.
• Je systém deterministický?
• Je systém neblokující?
• Je systém prakticky možný?
Úkol
• Formulujte paradox "Achilles a želva".
• Analyzujte chování hybridních automatu na následujícím slajdu.
IV120 Hybridní systémy - pokr.
str. 19/35
Příklady ZENO běhů
IV120 Hybridní systémy - pokr.
Príklady ZENO běhů
Nechť
o(x)-í «in (£) exp (-£)
PK ' ~ \ 0 if x = 0
pak
• následující hybridní systém má v intervalu (—e, 0] nekonečně mnoho průniků s osou x.
IV120 Hybridní systémy - pokr.
Analýza a syntéza hybridních systémů (HS)
Motivace modelování
» Cílem modelování HS je odvození vlastností reálných systémů z vlastností modelů, a syntéza kontrolérů (podmínek pro vykonání kontrolních událostí).
Verifikace
• Vykazuje hybridní systém popsaný hybridním automatem požadované chování (splňuje specifikaci)?
Syntéza
• Jestliže je možnost volby při návrhu systému, je možné tento návrh udělat tak, aby výsledný systém splňoval danou specifikaci?
IV120 Hybridní systémy - pokr.
str. 22/35
Validace
• Proces ověření, že teoretický návrh hybridním automatem se při praktické realizaci chová odpovídajícím způsobem.
• Vyhovující teoretický model, může být vzhledem k uvažovaným abstrakcím neimplementovatelný.
Obvyklé workflow
• Syntéza
• Verifikace
• Validace
IV120 Hybridní systémy - pokr.
Specifikace
Stabilita
» Typická vlastnost požadovaná v čistě spojitých systémech.
» Požadovat stabilitu hybridního systému vyžaduje definovat pojem stability v diskrétní složce.
Specifikace množinou stavů
• Specifikace bezpečných a zakázaných oblastí.
Specifikace množinou trajektorií
• Vlastnosti hybridních automatů, které se dají popsat vlastnostmi běhů.
• Množina povolených běhů hybridního automatu.
• Formální popis vlastností běhů s využitím modálních a temporálních logik. (CTL, LTL, CTL*).
IV120 Hybridní systémy - pokr.
str. 24/35
Metody analýzy
Deduktivní metody
• Matematické metody dokazování/odvozování vlastností hybridních systémů (matematická indukce).
• Nealgoritmizovatelné.
Model Checking
» Algoritmická procedura rozhodující, zda formálně popsaný hybridní systém splňuje formálně specifikované požadavky.
• Problém je rozhodnutelný pouze pro vybrané podtřídy hybridních automatů.
Softwarové simulace
• Používané za účelem výpočtu množiny Reach.
» Výsledek je často pouze aproximací skutečné množiny.
IV120 Hybridní systémy - pokr.
str. 25/35
Deduktivní metody - Invariantní množina
Použití deduktivních metod
• Typickým cílem metody je stanovit hranice množiny Reach skrze tzv.
• Invariantní množina je množina pro níž platí, že začne-li výpočet hybridního systému v dané množině, tak tuto množinu nikdy neopustí.
Definice invariantní množiny
• Množina stavů M C Q x X hybridního automatu H se nazýva invariantní pokud pro všechna (q, x) G M, všechna řešení
(r, q, x) začínající v (q, x), všechna /,- G r a všechna t G // platí, že (<7;(ŕ),x;(ŕ)) G M.
IV120 Hybridní systémy - pokr.
str. 26/35
Deduktivní metody - Vlastnosti invariantní množiny
Pozorování
• Sjednocení a průnik dvou invariantních množin automatu H jsou také invariantní množiny H.
» Pokud M je invariantní množina a Init C M, pak Reach C M.
Využití
• Je-li dána specifikace povolených stavů hybridního automatu (množina F), je možné identifikovat různé invariantní množiny splňující
Init C M C F
a pro účely přesného odhadu množiny Reach tyto proniknout. Cvičení
• Zdůvodněte výše uvedená tvrzení.
« Rozmyslete, jak postupovat při ukazování faktu, že nějaká množina M je invariantní množinou hybridního automatu H.
IV120 Hybridní systémy - pokr. str. 27/35
Model Checking
Zjednodušení
• V rámci tohoto kurzu se omezíme pouze na algoritmický test dosažitelnosti daného stavu pro vybrané podtřídy hybridních automatů.
Uvažované podtřídy hybridních automatů
• Časové automaty (TA).
• Rektangulární hybridní automaty (RHA).
• Lineární hybridní automaty (LHA).
Softwarové nástroje
• UPPAAL - časové automaty
• PHaVer - RHA, částečně LHA (HyTech)
IV120 Hybridní systémy - pokr.
str. 28/35
Časové automaty
Omezení
• Všechny derivace podle nichž se automat řídí při spojité evoluci stavu mají tvar:
d*i(t) = 1 dt
• V diskrétní složce je navíc položeno omezení na R, kdy je dovoleno bud' ponechat stávající hodnotu spojité proměnné, nebo ji „nastavit" na jinou celočíselnou hodnotu (typicky 0).
• Dom a G definováno pouze s použitím relací < a > na celočíselných hodnotách.
Intuice
• Konečný automat s množinou spojitých proměnných pro měření uplynulého času.
• Měřené hodnoty je možné resetovat při provedení diskrétního přechodu.
IV120 Hybridní systémy - pokr.
str. 29/35
Časové automaty příklad
Příklad časového automatu
Cvičení
» Zakreslete vývoj hodnot spojitých proměnných v čase.
• Na dvourozměrném grafu s osami x\ a x2 ukažte jak se mění hodnoty proměnných v čase.
• Jak se projeví fakt, že dovolíme pouze resety na hodnotu 0?
IV120 Hybridní systémy - pokr.
str. 30/35
Regionová abstrakce
Klíčové pozorování
• Vzhledem k tomu, že všechna porovnání v časových
automatech jsou celočíselná, automat není schopen rozlišit dvě různé hodnoty spojité proměnné se stejnou celočíselnou částí.
Třídy ekvivalence na spojité doméně
« Je-li c nejvyšší celé číslo, na které je spojitá proměnná porovnávána, pak lze tuto spojitou proměnnou ekvivalentně reprezentovat jednou hodnotou z následující posloupnosti:
[0], (0,1), [1], (1, 2), [2],... [c - 1], (c - 1, c), [c], (c, oo)
» Abstrahovaná doména je konečná pro každou proměnnou.
• Lze sestrojit konečný automat, který věrně simuluje časový automat a otázku verifikace algoritmicky rozhodnout nad tímto konečným automatem.
IV120 Hybridní systémy - pokr. str. 31/35
Regionová abstrakce
IV120 Hybridní systémy - pokr.
str. 32/35
Rektangulární hybridní automaty (RHA)
Omezení
• Všechny derivace podle nichž se automat řídí při spojité evoluci stavu mají tvar:
kde a a b jsou racionální konstanty.
• Při specifikaci automatu se neuvádí diferenciální rovnice, ale pouze konstanty a a b, jakožto krajní meze.
Cvičení
« Uvažte rektangulární automat s dvěmi spojitými proměnnými xi a x2 . Na dvojrozměrném grafu s osami x\ a x2 demonstrujte vývoj hodnot proměnných, který odpovídá spojité evoluci.
• Odkud pochází název této třídy hybridních automatů?
IV120 Hybridní systémy - pokr. str. 33/35
Algoritmická rozhod n utelnost RHA
Dosažitelnost
• Problém dosažitelnosti daného stavu z konkrétního daného iniciální stavu je rozhodnutelný, pokud diskrétní přechody automatu resetují (reinicializují) hodnoty proměnných na konečnou množinu konkrétních hodnot.
» Největší známá rozhodnutelná podtřída RHA.
Nerozhodnutelnost
» Relaxace od přesných reinicializací vede k podtřídě hybridních automatů, pro níž je problém dosažitelnosti nerozhodnutelný.
IV120 Hybridní systémy - pokr.
str. 34/35
Lineární hybridní automaty (LHA)
Definice
» Pokud ko,... ,km jsou definované konstanty a xi,... ,xm proměnné, pak výraz tvaru ko + k\X\ + k2x2 + • • • + kmxm se nazývá lineární výraz.
• Pokud ri, t2 jsou lineární výrazy pak výraz tvaru t\ < t2 se nazývá lineární nerovnost.
9 Hybridní automat H se nazývá , pokud /n/ŕ, Dom, G
a ŕ" jsou definovány jako boolovské kombinace lineárních nerovností.
Nerozhodnutelnost
• Problém dosažitelnosti stavu je pro LHA nerozhodnutelný.
• Dokázáno redukcí z problému zastavení.
• Implementované algoritmy negarantují terminaci (HyTech).
IV120 Hybridní systémy - pokr.
str. 35/35