Reachability Analysis for Timed Models using Max-Plus Algebra
Authors
Lu, Qi ; Madsen, Michael ; Ravn, Søren
Term
2. term
Education
Publication year
2011
Submitted on
2011-06-09
Pages
49
Abstract
Dette speciale undersøger brugen af max-plus-polyedre—mængder defineret i max-plus algebra—til at repræsentere klokkerummet ved nåbarhedstjek i tidsmodeller. Overapproksimation betyder at analysere en større, enklere mængde, der indeholder det præcise klokkerum. Vi viser, at der findes modeller, hvor max-plus-overapproksimation er nøjagtig, mens DBM (Difference Bound Matrices) overapproksimation ikke er det. Vi beviser en ekstrapolationsalgoritme for endimensionale max-plus-polyedre og skitserer principperne for en generel ekstrapolationsalgoritme. Vi implementerer max-plus-polyedre-repræsentationen i en modeltjekker for timed-arc Petri nets og viser, at for nogle modeller, hvor DBM-overapproksimation ikke giver korrekte resultater, kan max-plus-overapproksimation være hurtigere end en eksakt DBM-analyse.
This thesis examines using max-plus polyhedra—sets defined in max-plus algebra—to represent the space of clock values when checking whether states are reachable in timed models. Overapproximation means analyzing a larger, simpler set that contains the exact clock space. We show that there are models where max-plus overapproximation is exact, while DBM (Difference Bound Matrices) overapproximation is not. We prove an extrapolation algorithm for single-dimensional max-plus polyhedra and outline principles toward a general extrapolation algorithm. We implement the max-plus polyhedra representation in a model checker for timed-arc Petri nets and demonstrate that, for some models where DBM overapproximation fails to give correct results, max-plus overapproximation can be faster than exact DBM analysis.
[This abstract was generated with the help of AI]
Documents
Other projects by the authors
Lu, Qi:
Madsen, Michael:
Ravn, Søren: