LU, Qi, Michael MADSEN, Martin MILATA, Søren RAVN, Uli FAHRENBERG and Kim G. LARSEN. Reachability analysis for timed automata using max-plus algebra. Journal of Logic and Algebraic Programming. Holland: Elsevier, 2012, vol. 81, No 3, p. 298-313. ISSN 1567-8326. doi:10.1016/j.jlap.2011.10.004.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name Reachability analysis for timed automata using max-plus algebra
Name in Czech Analýza dosažitelnosti pro časové automaty s použitím max-plus algebry
Authors LU, Qi (156 China), Michael MADSEN (208 Denmark), Martin MILATA (203 Czech Republic, guarantor, belonging to the institution), Søren RAVN (208 Denmark), Uli FAHRENBERG (276 Germany) and Kim G. LARSEN (208 Denmark).
Edition Journal of Logic and Algebraic Programming, Holland, Elsevier, 2012, 1567-8326.
Other information
Original language English
Type of outcome Article in a journal
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher Denmark
Confidentiality degree is not subject to a state or trade secret
WWW URL
Impact factor Impact factor: 0.529
RIV identification code RIV/00216224:14330/12:00059430
Organization unit Faculty of Informatics
Doi http://dx.doi.org/10.1016/j.jlap.2011.10.004
UT WoS 000302500700008
Keywords in English Timed automaton; Real-time model checking; Data structure; Max-plus algebra; Max-plus polyhedron
Tags International impact, Reviewed
Changed by Changed by: RNDr. Pavel Šmerk, Ph.D., učo 3880. Changed: 22. 4. 2013 23:06.
Abstract
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.
Abstract (in Czech)
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.
Links
LA09016, research and development projectName: Účast ČR v European Research Consortium for Informatics and Mathematics (ERCIM) (Acronym: ERCIM)
Investor: Ministry of Education, Youth and Sports of the CR, Czech Republic membership in the European Research Consortium for Informatics and Mathematics
MUNI/A/0914/2009, interní kód MUName: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace (Acronym: SV-FI MAV)
Investor: Masaryk University, Category A
PrintDisplayed: 27. 5. 2022 05:59