Room P3.10, Mathematics Building

Manuel Biscaia, SQIG - Instituto de Telecomunicações
Verification of Markov chains and its relation to the Skolem Problem

When studying probabilistic dynamical systems, temporal logic has typically been used to reason about path properties. Recently, there has been some interest in reasoning about the dynamical evolution of state probabilities of these systems. In this paper we show that verifying linear temporal properties concerning the state evolution induced by a Markov chain is equivalent to the decidability of the Skolem problem — a long standing open problem in Number Theory. However, from a practical point of view, usually it is enough to check properties up to some acceptable error bound. We show that an approximate version of Skolem problem is decidable, and that it can be applied to verify, up to an arbitrarily small error, linear temporal properties of the state evolution induced by a Markov chain.