Efficient Model Checking for Probabilistic Timed Automata
Authors
Engdahl, Robert Jørgensgaard ; Haugstad, Arild Martin Møller
Term
2. term
Education
Publication year
2008
Abstract
Denne afhandling undersøger netværk af probabilistiske tidsautomater, en måde at modellere systemer på hvor timing (forsinkelser og tidsfrister), samtidighed og synkronisering samt probabilistisk adfærd fra systemet eller dets omgivelser er vigtige. Vi præsenterer en fremadrettet udforskning og reduktionsalgoritme for tilstandsrum, som opdeler tilstandsrum for både probabilistiske og almindelige tidsautomater efter tids-abstrakte ækvivalenser (dvs. grupperer tilstande, der opfører sig ens uanset præcise tidsstempler). Vi viser, hvordan denne opdeling kan bruges til at beregne probabilistisk nåbarhed, herunder maksimale nåbarhedssandsynligheder. Vi har implementeret en prototype, Uppaal Prob, som en udvidelse til værktøjet Uppaal Prob. Den omfatter tilstandsrum-udforskning og -reduktion, forfining baseret på probabilistiske nåbarhedsformler og beregning af maksimale nåbarhedssandsynligheder.
This thesis studies networks of probabilistic timed automata, a way to model systems where timing (delays and timeouts), concurrency and synchronization, and probabilistic behavior from the system or its environment all matter. We present a forward state-space exploration and reduction algorithm that partitions the state space of both probabilistic and standard timed automata according to time-abstract equivalences (i.e., grouping states that behave the same regardless of exact timestamps). We show how this partitioning can be used to compute probabilistic reachability, including maximal probabilities of reaching target states. We implemented a prototype tool, Uppaal Prob, as an extension to the Uppaal Prob tool. It includes the state-space exploration and reduction algorithm, refinement guided by probabilistic reachability formulae, and computation of maximal reachability probabilities.
[This abstract was generated with the help of AI]
Documents