Reachability Analysis for Timed Models using Max-Plus Algebra

Student thesis: Master thesis (including HD thesis)

  • Qi Lu
  • Michael Madsen
  • Søren Ravn
2. term, Computer Science, Master (Master Programme)
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.
Publication date9 Jun 2011
Number of pages49
ID: 52850498