On the automatic verification of Distributed Probabilistic Automata with Partial Information
| Title | On the automatic verification of Distributed Probabilistic Automata with Partial Information |
| Publication Type | Thesis |
| Year of Publication | 2010 |
| Authors | Giro, S |
| Academic Department | FaMAF |
| Degree | PhD |
| University | Universidad Nacional de Córdoba |
| City | Córdoba |
| Thesis Type | PhD |
| Abstract | We study concurrent systems involving probabilities and non-determinism. Specifically, we focus on the automatic verification of distributed systems, in which each component can access only a limited portion of the information in the system. Although model checking algorithms for Markov decision processes (MDPs) can be applied to distributed systems, such algorithms assume that all components in the system have access to all the information. As a consequence, some correct distributed systems are deemed incorrect when we analyse them using algorithms for MDPs. In this thesis, we present model checking algorithms for distributed systems involving probabilities and nondeterminism. A relevant contribution is the result that there exists no algorithm to solve the model checking problem in a completely automated fashion. That is, there exist no algorithm so that, for all distributed systems and properties, the algorithm decides whether the property holds or not. Despite of this result, we present two algorithms: one of these algorithms is able to detect that some systems are correct, while the other detects incorrect ones. In addition, we present a new adaptation of the POR technique. Our adaptation profits from the fact that a component in a concurrent system has limited access to the information stored by other components. Our technique provides more effective reductions than those obtained using existing techniques for MDPs. We conclude the thesis by presenting case studies in which our algorithms yield better results when compared to their counterparts for MDPs. |
PDF (Full text):
