Reachability analysis for timed automata using max-plus algebraReportar como inadecuado




Reachability analysis for timed automata using max-plus algebra - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

1 CISS - Center for Indlejrede Software Systemer 2 ESTASYS - Efficient STAtistical methods in SYstems of systems Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL

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.

Keywords : timed automaton real-time model checking data structure max-plus algebra max-plus polyhedron





Autor: Qi Lu - Michael Madsen - Martin Milata - Søren Ravn - Uli Fahrenberg - Kim Guldstrand Larsen -

Fuente: https://hal.archives-ouvertes.fr/



DESCARGAR PDF




Documentos relacionados