A master thesis from Aalborg University
Reachability Analysis for Timed Models using Max-Plus Algebra
Author(s)
Term
2. term
Education
Publication year
2011
Submitted on
2011-06-08
Pages
49 pages
Abstract
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.
Documents
Colophon: This page is part of the AAU Student Projects portal, which is run by Aalborg University. Here, you can find and download publicly available bachelor's theses and master's projects from across the university dating from 2008 onwards. Student projects from before 2008 are available in printed form at Aalborg University Library.
If you have any questions about AAU Student Projects or the research registration, dissemination and analysis at Aalborg University, please feel free to contact the VBN team. You can also find more information in the AAU Student Projects FAQs.