Reachability analysis for timed automata using max-plus algebra

Varování

Publikace nespadá pod Ústav výpočetní techniky, 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 http://dx.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
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:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.

Další info