Reachability analysis for timed automata using max-plus algebra

• 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
• 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

• 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