Algoritmická analýza systémů s celočíselnými
registry
Petr Novotný
Fakulta informatiky Masarykova Univerzita Brno
24. října 2011
Petr Novotný Algoritmická analýza systémů s celočíselnými registry
Přehled
Q Model stroje s čítači
O Příklady modelovaných systémů
• aneb fronty a roboti.
• Jaké otázky chceme algoritmicky řešit?
O Přehled výsledků (dřívějších i nových) O Směry budoucího vývoje
• aneb palivo (bohužel) neroste na stromech.
Petr Novotný Algoritmická analýza systémů s celočíselnými registry
Stroje s čítači
1/2: DEC(Ci)
DEC(Ci) INC(C2)
• Qo stochastické stavy (o), Q1 kontrolovatelné stavy (o).
• Kontrolér: a: ((Q0 U xN'-> V(Q)
Petr Novotný Algoritmická analýza systémů s celočíselnými registry
Algoritmické otázky
Cíl: formálně vyjádřená vlastnost, kterou by měl systém ovládaný kontrolérem splňovat. Otázky:
• Existuje kontrolér, který zajistí splnění cíle?
• Jak moc musí být takový kontrolér složitý?
• Lze algoritmicky:
• Rozhodnout o existenci takového kontroléru?
• Zkonstruovat tento kontrolér?
Petr Novotný Algoritmická analýza systémů s celočíselnými registry
Teorie front
Cílem je
• Vynulovat čítač (terminovat) s co největší pravděpodobností (ideálně 1).
• Učinit tak co nejrychleji.
Petr Novotný Algoritmická analýza systémů s celočíselnými registry
Energetické hry
systém
prostředí
Cílem je
o Ovládat systém tak, aby se nikdy nevyčerpal žádný zdroj. • Učinit tak s co možná nejmenšími „nádržemi".
Petr Novotný Algoritmická analýza systémů s celočíselnými registry
Terminace - známé výsledky
Pouze případ s jedním čítačem. Existují polynomiální algoritmy, které:
• rozhodují, zda je možné v daném systému terminovat s pravděpodobností 1 (+ konstrukce bezčítačového bezpaměťového deterministického kontroléru);
O  T. Brázdil, V. Brožek, K. Etessami, A. Kučera, D. Wojtczak: One-counter Markov Decision Processes. SODA 2010.
• pro zadaný kontrolér aproximují průměrný čas na vynulování čítače (s libovolnou přesností).
•  T. Brázdil, S. Kiefer, A. Kučera: Efficient Analysis of Probabilistic Programs with an Unbounded Counter. CAV 2011.
Petr Novotný Algoritmická analýza systémů s celočíselnými registry
Terminace - nové výsledky
Verifikace —> syntéza.
• EXPTIME algoritmus pro aproximaci minimálního průměrného času. (+ konstrukce konečně paměťové deterministické strategie).
• N P i coNP těžkost.
• Na rozumných instancích má algoritmus lepší složitost.
Petr Novotný Algoritmická analýza systémů s celočíselnými registry
Energetické hry - známé výsledky
Pouze nestochastický případ.
Existence a syntéza „bezpečného" kontroléru:
• Obecně EXPSACE těžké.
• Pro k čítačů (k - 1)-EXPTIME algoritmus, o Pro 1 čítač polynomiální algoritmus.
• T. Brázdil, P. Jančar: Reachability Games on Extended Vector Addition Systems with States. ICALP 2010.
• Pro 2 čítače polynomiální algoritmus.
• J. Chaloupka: Z-reachability Problem for Games on 2-dimensional Vector Addition Systems with States is in P. In Reachability Problems.
Výpočet potřebné velikosti čítače:
• Projeden čítač polynomiální algoritmus ověřující, že zadaná kapacita čítače stačí.
• P. Bouyer, U. Fahrenberg, K. G. Larsen, N. Markey, J. Srba: Infinite runs in weighted timed automata with energy constraints. FORMATS 2008.
Petr Novotný Algoritmická analýza systémů s celočíselnými registry
Nový pohled - energie není zadarmo
DEC(Ci)
palivo: l$/l
Ci: palivo
• Primární cíl: bezpečná kontrola (nevyčerpá se palivo).
• Sekundární cíle: minimální nutná velikost nádrže a minimální průměrná cena za 1 krok.
Sekundární cíle jdou proti sobě =4> Paretovská optimalizace.
Petr Novotný Algoritmická analýza systémů s celočíselnými registry
aver
9 Model stroje s čítači je přirozený a mnohostranně využitelný
(fronty, energie). 0 Dají se pomocí něj hledat odpovědi na přirozené otázky:
• čas výpočtu - terminování,
• bezpečná kontrola systémů závislých na vlastní zásobě energie,
• otázky systémového návrhu - optimální kapacita zásob,
• ekonomická optimalizace provozu.
O Mnohé z těchto otázek lze řešit efektivními algoritmy. Má tedy smysl další takové algoritmy hledat.
O Rozšíření o ekonomický pohled.
Petr Novotný Algoritmická analýza systémů s celočíselnými registry