On the verification of probabilistic I/O automata with unspecified rates
Sergio Giro, Pedro R. D’Argenio · 2009
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 over-estimation computed over the PIOA gives a more realistic result than the exact computation over the MDP.