ANALÝZA HYBRIDNÍCH SYSTÉMŮSeminář Sybily, 4.3.2011

Osnova Definice HS Problémy Přehled přístupů Přehled existujících nástrojů

Hybridní automat Módy (mají invarianty=části prostoru) Každý mód má svou (spojitou) dynamiku

Konstantní derivace Lineární Nelineární (např. multiafinní)

+diskrétní přechody mezi módy

Často se řeší otázka reachability (resp. safety)

Problémy Curse of dimensionality Wrapping effect

Po částech konstantní derivace (Linear Hybrid Automata)

Lineární systémy Nelineární systémy

Přístupy Direct – přímý výpočet reachable

množiny Indirect – pomocí diskrétní abstrakce

stavového prostoru

Nástroje MARCO (Hsolver), Ariadne (CheckMate, HyTech), PHAVer SpaceEx MATISSE

LHA Po částech konstantní omezení derivací

(dynamika - diferenciální inkluze)

Přechody – spojitý posun v čase; diskrétní Reachability pomocí fixed-point

Množiny reprezentovány pomocí polyedrů PHAVer

PHAVer (nástupce HyTechu) - 2005 - G. Frehse převod hybridizací lineárních systémů

na lineární hybridní automaty (LHA), safety verification

stejně jak HyTech má uložená data jako konvexní mnohostěny (polyhedra)

používá Parma Polyhedra Library Příklady: Hsolver x PHAVer - 4D

PHAVer Polyedry – hodně hranic, s velkými

koeficienty

Omezení počtu bitů zadávajících hranice, lineární programování - overaproximace

Jen K nejvýznamnějších hranic (overaproximace, angle reconstruction)

PHAVer

PHAVer – forward/backward

Lineární systémy Tvar: U je

konvexní

vývoj s časovým krokem r: Overaproximace:

Reprezentace dosažené množiny

Reprezentace množin a operace

SpaceEx 2011 - Frehse, Guernic, Donzé, Ray, Lebeltel, Ripado,

Girard, Dang, Maler scalable reachability, pro po částech afinní

(nedeterm. dynamika) hybridní systémy Reprezentace množin: support functions + template

polyhedra Lineární - 100D a víc, (324s box), resp. 16D (1236s

octagonal), Nelineární - 12D pokud se použijou aproximační

techniky pro nelineární (Dang, Maler, Testylier, Guernic - např. čl. Accurate hybridization of nonlinear systems)

SpaceEx

MATISSE 2005 Redukuje dimenzi lineárního systému s

ohraničeními (constrained linear system)

Aproximační bisimulace systém~redukce Matlab toolbox, používá semidefinitní prg

SEDUMI a manipulaci s mnohostěny YALMIP 10D 6D, 4D

Nelineární systémy Forma (f je L-Lipschitzovská)

Aproximace po částech

části: simplexy, boxy, pohyblivé simpl./boxy

SpaceEx (hybridizace), MARCO (multiafinizace), Ariadne (interval arithmetic)

MARCO 2007 - Ádam Halász, Vijay Kumar pro multiaffinní hybridní systémy (HMS=hyper-rectangular multi-

affine switched systém) Dosažitelné množiny v módech jsou uložené jako polyhedrální

množiny. Termination conditions:

1. nově dosažená množina v módu je podmnožina předchozí dosažené množ.

2. pokud je objem nově spočítané dosažitelné množiny menší než v předchozí iteraci a tvoří jen malou část celkového prostoru (malá konstanta . objem celého uvažovaného prostoru)

3. když vyleze vypočítaná množina ven z uvažovaných hranic algoritmus napsaný v MATLABu (používá free Multiparametric

toolbox) 4D ... 120s

MARCO

Ariadne 2008, (o něco lepší než Hsolver pro ODE) -

Collins, Goldsztejn Rigorous reachability analysis pro

nenlineární systémy, interval analysis based algorithm Reach and

Evolve (interval integration, aproximace Taylorovou řadou se známou chybou)

výsledky - systém se dvěma oscilacemi, které se jiným nástrojům nepodařilo rigorózně oddělit

Přehled nástrojů

Nástroj Rok Systémy #proměnných

PHAVer 2005 LHA,Lineární systémy

4D

SpaceEx 2011 Piecewise affine,Nelineární systémy

100D lin,16D nonlin

MATISSE 2007 Constrained lineární sys.,Redukce

10D

MARCO 2007 Piecewise multiaffine,Nelineární

4D

Ariadne 2008 Nelineární systémy 2D

Literatura Recent progress in Continuous and Hybrid Reachability Analysis (Asarin,

Dang, Frehse, Girard, Guernic, Maler) 2006. The Reach-and-Evolve Algorithm for Reachability Analysis of Nonlinear

Dynamical Systems (Collins) 2008. Approximate bisimulation relations for constrained linear systems (Girard,

Pappas) 2007. MARCO: A Reachability Algorithm for Multi-Affine Systems with

Applications to Biological Systems (Berman, Halász, Kumar) 2007. An evaluation of two recent reachability analysis tools for hybrid systems

(Makhlouf, Kowalewski) 2006. PHAVer: Algorithmic Verification of Hybrid Systems past HyTech (Frehse)

2005. Computing Reachable Sets for Nonlinear Biological Models (Dang,

Guernic, Maler) 2009. Accurate Hybridization of Nonlinear Systems (Dang, Maler, Testylier) 2010. SpaceEx: Scalable Verification of Hybrid Systems (Frehse, Guernic, Donzé,

Ray, Lebeltel, Ripado, Girard, Dang, Maler) 2011.