Logic and model checking for hidden Markov models


Zhang, Lijun and Hermanns, Holger and Jansen, David N. (2005) Logic and model checking for hidden Markov models. In: International Conference on Formal Techniques for Networked and Distributed Systems, FORTE 2005, October 2-5, 2005, Taipei, Taiwan (pp. pp. 98-112).

open access
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.
Item Type:Conference or Workshop Item
Additional information:ZHJ05
Copyright:© 2005 IFIP International Federation for Information Processing
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/54796
Official URL:https://doi.org/10.1007/11562436_9
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page

Metis ID: 229285