A Decidable Probability Logic for Timed Probabilistic Systems

Article type: Research Article

Authors: Lanotte, Ruggero | Beauquier, Danièle

Affiliations: Dipartimento di Scienze della Cultura, Politiche e dell'Informazione Università dell'Insubria, Italy. E-mail: ruggero.lanotte@uninsubria.it | LACL CNRS FRE 2673, Université Paris 12 Val de Marne, France

Abstract: In this paper we extend the predicate logic introduced by Beauquier et al. in order to deal with Markov decision processes. We prove that with respect to qualitative probabilistic properties, model checking is decidable for this logic applied to Markov decision processes. Furthermore we apply our logic to probabilistic timed transition systems using predicates on clocks. We prove that results on Markov decision processes hold also for probabilistic timed transition systems. The interest of this logic lies in particular on the fact that some important properties are expressible in this logic but not expressible in pCTL.

Keywords: Markov Decision Processes, Probabilistic Timed Transition Systems, Model Checking, Predicate logic of Probabilities

DOI: 10.3233/FI-2009-171

Journal: Fundamenta Informaticae, vol. 96, no. 1-2, pp. 127-151, 2009