On the verification of probabilistic I/O automata with unspecified rates

TitleOn the verification of probabilistic I/O automata with unspecified rates
Publication TypeConference Paper
Year of Publication2009
AuthorsGiro, S, D'Argenio, PR
Conference NameProceedings of the 2009 ACM Symposium on Applied Computing (SAC)
PublisherACM
ISBN Number978-1-60558-166-8
AbstractWe consider the Probabilistic I/O Automata framework, for which we address the verification of reachability properties in case the rates (also called delay parameters) are unspecified. We show that the problem of finding (or even approximating) the supremum probability that a set of states is reached is undecidable. However, we give an algorithm to obtain a non-trivial over-estimation of this value. We explain why this over-estimation may result useful for many systems. Finally, in order to compare our approach against Markov Decision Processes, we study a simple protocol for anonymous fair service. In this case, the over-estimation computed over the PIOA gives a more realistic result than the exact computation over the MDP.
DOI10.1145/1529282.1529406
PDF (Full text):