Reachability analysis for timed automata using max-plus algebra

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.
Type de document :
Article dans une revue
The Journal of Logic and Algebraic Programming, 2012, 81, pp.298 - 313. 〈10.1016/j.jlap.2011.10.004〉
Liste complète des métadonnées

Littérature citée [32 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01087998
Contributeur : Uli Fahrenberg <>
Soumis le : jeudi 27 novembre 2014 - 10:59:25
Dernière modification le : mercredi 16 mai 2018 - 11:24:07
Document(s) archivé(s) le : lundi 2 mars 2015 - 09:20:43

Fichier

jlp.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Qi Lu, Michael Madsen, Martin Milata, Søren Ravn, Uli Fahrenberg, et al.. Reachability analysis for timed automata using max-plus algebra. The Journal of Logic and Algebraic Programming, 2012, 81, pp.298 - 313. 〈10.1016/j.jlap.2011.10.004〉. 〈hal-01087998〉

Partager

Métriques

Consultations de la notice

304

Téléchargements de fichiers

129