Reachability Analysis for Timed Models using Max-Plus Algebra

Studenteropgave: Speciale (inkl. HD afgangsprojekt)

  • Qi Lu
  • Michael Madsen
  • Søren Ravn
2. semester, Datalogi, Kandidat (Kandidatuddannelse)
In this report, we elaborate on the work done on showing max-plus polyhedra capable of representing the clock space for reachability checking of timed models. We show that there exist models where max-plus overaproximation is exact, but DBM overapproximation is not. We prove an extrapolation algorithm for single-dimensional max-plus polyhedra, and describe principles for an extrapolation algorithm for general max-plus polyhedra. Finally, we implement our max-plus polyhedra representation on top of a model checker for timed-arc Petri nets, and show that for some models where DBM overapproximation fails to provide correct results, max-plus overapproximation is faster than exact DBM analysis.
Udgivelsesdato9 jun. 2011
Antal sider49
ID: 52850498