On Zone-Based Analysis of Duration Probabilistic Automata

Oded Maler
(CNRS-VERIMAG,University of Grenoble, France)
Kim G. Larsen
(CISS and CS Aalborg University, Denmark)
Bruce H. Krogh
(Department of EC Carnegie Mellon University, USA)

We propose an extension of the zone-based algorithmics for analyzing timed automata to handle systems where timing uncertainty is considered as probabilistic rather than set-theoretic. We study duration probabilistic automata (DPA), expressing multiple parallel processes admitting memoryfull continuously-distributed durations. For this model we develop an extension of the zone-based forward reachability algorithm whose successor operator is a density transformer, thus providing a solution to verification and performance evaluation problems concerning acyclic DPA (or the bounded-horizon behavior of cyclic DPA).

In Yu-Fang Chen and Ahmed Rezine: Proceedings 12th International Workshop on Verification of Infinite-State Systems (INFINITY 2010), Singapore, 21st September 2010, Electronic Proceedings in Theoretical Computer Science 39, pp. 33–46.
Published: 28th October 2010.

ArXived at: http://dx.doi.org/10.4204/EPTCS.39.3 bibtex PDF

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org