Reachability Analysis for Timed Automata using Max-Plus Algebra
Authors
Lu, Qi ; Madsen, Michael ; Milata, Martin ; Ravn, Søren
Term
1. term
Education
Publication year
2011
Submitted on
2011-01-17
Pages
34
Abstract
Dette speciale undersøger brugen af max-plus-polyedre som datastruktur til at repræsentere klokkerummet – mængden af alle mulige klokkeværdier – i nåbarhedsanalyse af timede automater (matematiske modeller af systemer med tidsadfærd). Med afsæt i det omfattende arbejde med difference bound matrices og tidligere anvendelser af max-plus-polyedre i andre områder færdiggør vi de algoritmer, der kræves til både fremadrettet nåbarhed (hvilke tilstande kan nås fra start) og bagudrettet nåbarhed (om en måltilstand kan nås). Vi giver formelle beviser for, at disse algoritmer er korrekte i forhold til definitionerne af de underliggende operationer. For at vise at tilgangen fungerer i praksis såvel som i teori laver vi en proof-of-concept-implementering oven på modelcheckeren opaal.
This thesis explores using max-plus polyhedra as a data structure to represent the clock space—the set of all possible clock values—in the reachability analysis of timed automata (mathematical models of systems with timing). Building on extensive work with difference bound matrices and prior uses of max-plus polyhedra in other areas, we complete the algorithms needed for both forward reachability (what states can be reached from the start) and backward reachability (whether a target state can be reached). We provide formal proofs that these algorithms are correct according to the definitions of the underlying operations. To show that the approach works in practice as well as in theory, we build a proof-of-concept implementation on top of the opaal model checker.
[This abstract was generated with the help of AI]
Documents
Other projects by the authors
Lu, Qi:
Madsen, Michael:
Ravn, Søren: