Reachability analysis for timed automata using max-plus algebra

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.

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

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 project: Name: Úč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 MU: Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace (Acronym: SV-FI MAV)

Investor: Masaryk University, Category A