Logic and Model Checking for Hidden Markov Models
In Formal Techniques for Networked and Distributed Systems (FORTE)
, pages 98-112, Springer
, Lecture Notes in Computer Science 3731, 2005.
Downloads: pdf, bibURL: http://dx.doi.org/10.1007/11562436_9
Abstract. The branching-time temporal logic PCTL^* has been introduced to specify quantitative properties over probability systems, such as discrete-time Markov chains. Until now, however, no logics have been defined to specify properties over hidden Markov models (HMMs). In HMMs the states are hidden, and the hidden processes produce a sequence of observations. In this paper we extend the logic PCTL^* to POCTL^*. With our logic one can state properties such as “there is at least a 90 percent probability that the model produces a given sequence of observations” over HMMs. Subsequently, we give model checking algorithms for POCTL^* over HMMs.