[ZhangHJ05] Logic and Model Checking for Hidden Markov Models Zhang, L.; Hermanns, H. and Jansen, D. N. In Formal Techniques for Networked and Distributed Systems (FORTE), pages 98-112, Springer, Lecture Notes in Computer Science 3731, 2005.
Downloads: pdf, bibURL: 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.