Reachability analysis for timed automata using max-plus algebra

Varování

Publikace nespadá pod Filozofickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.

Název česky	Analýza dosažitelnosti pro časové automaty s použitím max-plus algebry
Autoři	LU Qi MADSEN Michael MILATA Martin RAVN Soren FAHRENBERG Uli LARSEN Kim G.
Rok publikování	2012
Druh	Článek v odborném periodiku
Časopis / Zdroj	Journal of Logic and Algebraic Programming
Fakulta / Pracoviště MU	Fakulta informatiky
Citace
www	http://www.sciencedirect.com/science/article/pii/S156783261100097X
Doi	https://doi.org/10.1016/j.jlap.2011.10.004
Obor	Informatika
Klíčová slova	Timed automaton; Real-time model checking; Data structure; Max-plus algebra; Max-plus polyhedron
Přiložené soubory	maxplus-paper.pdf
Popis	Ukážeme, že max-plus mnohostěny lze využít jako datovou strukturu v analýze dosažitelnosti v časových automatech. Navrhujeme algoritmus pro analýzu dopředné i zpětné dosažitelnosti, který využívá max-plus mnohostěny namísto dříve používaných matic reprezentujících omezení rozdílů proměnných (difference bound matrices). Funkčnost nového přístupu byla prokázána pomocí experimentální implementace využívající nástroj pro ověřování modelu opaal.
Související projekty:	Účast ČR v European Research Consortium for Informatics and Mathematics Rozsáhlé výpočetní systémy: modely, aplikace a verifikace