@conference {DBLP:conf/sac/GiroD09,
title = {On the verification of probabilistic I/O automata with unspecified rates},
booktitle = {Proceedings of the 2009 ACM Symposium on Applied Computing (SAC)},
year = {2009},
pages = {582-586},
publisher = {ACM},
organization = {ACM},
abstract = {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.},
isbn = {978-1-60558-166-8},
doi = {10.1145/1529282.1529406},
author = {Sergio Giro and Pedro R. D{\textquoteright}Argenio}
}