on 31-10-2014
The talk of Manuel Biscaia had to be postponed to this Friday, October 31. To Manuel and to the participants my apologies for the inconvenience.
Verification of Markov chains and its relation to the Skolem Problem
Manuel Biscaia, SQIG - Instituto de Telecomunicações
October 31, 2014, Friday, 16h15m.
Abstract: 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.
L states that whenever {γ1,…,γk}⊢Lα there is a proof in which each formula occurrence is either a sub-formula of α or of some of γi. In this work we extend Statman's result and show that any propositional (possibly modal) structural logic satisfying a particular statement of the sub-formula principle is PSPACE-complete. As a consequence, EXPTIME-complete propositional logics, such as PDL and the common-knowledge epistemic logic with at least 2 agents satisfy this particular sub-formula principle, if and only if, PSPACE=EXPTIME.
Room: 3.10, Mathematics
Support: SQIG/Instituto de Telecomunicações with support from FCT and FEDER namely by the FCT project PEst-OE/EEI/LA0008/2013.