LU, Qi, Michael MADSEN, Martin MILATA, Søren RAVN, Uli FAHRENBERG a Kim G. LARSEN. Reachability analysis for timed automata using max-plus algebra. Journal of Logic and Algebraic Programming. Holland: Elsevier, 2012, roč. 81, č. 3, s. 298-313. ISSN 1567-8326. doi:10.1016/j.jlap.2011.10.004.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název 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 (156 Čína), Michael MADSEN (208 Dánsko), Martin MILATA (203 Česká republika, garant, domácí), Søren RAVN (208 Dánsko), Uli FAHRENBERG (276 Německo) a Kim G. LARSEN (208 Dánsko).
Vydání Journal of Logic and Algebraic Programming, Holland, Elsevier, 2012, 1567-8326.
Další údaje
Originální jazyk angličtina
Typ výsledku Článek v odborném periodiku
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Dánsko
Utajení není předmětem státního či obchodního tajemství
WWW URL
Impakt faktor Impact factor: 0.529
Kód RIV RIV/00216224:14330/12:00059430
Organizační jednotka Fakulta informatiky
Doi http://dx.doi.org/10.1016/j.jlap.2011.10.004
UT WoS 000302500700008
Klíčová slova anglicky Timed automaton; Real-time model checking; Data structure; Max-plus algebra; Max-plus polyhedron
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 22. 4. 2013 23:06.
Anotace
We show that max-plus polyhedra are usable as a data structure in reachability analysis of timed automata. Drawing inspiration from the extensive work that has been done on difference bound matrices, as well as previous work on max-plus polyhedra in other areas, we develop the algorithms needed to perform forward and backward reachability analysis using max-plus polyhedra. To show that the approach works in practice and theory alike, we have created a proof-of-concept implementation on top of the model checker opaal.
Anotace česky
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.
Návaznosti
LA09016, projekt VaVNázev: Účast ČR v European Research Consortium for Informatics and Mathematics (ERCIM) (Akronym: ERCIM)
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Účast ČR v European Research Consortium for Informatics and Mathematics
MUNI/A/0914/2009, interní kód MUNázev: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace (Akronym: SV-FI MAV)
Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
VytisknoutZobrazeno: 8. 8. 2022 16:18