On the Verification of Probabilistic I/O Automata with Unspecified Rates

SERGIO GIRO; PEDRO R. D'ARGENIO

Hawai

Simposio; 24th Annual ACM Symposium on Applied Computing; 2009

ACM

We 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 overestimation computed over the PIOA gives a more realistic result than the exact computation over the MDP.