Logic and model checking for hidden Markov models

Share/Save/Bookmark

Zhang, L. and Hermanns, H. and Jansen, D.N. (2005) Logic and model checking for hidden Markov models. In: Formal techniques for networked and distributed systems, FORTE.

[img]
Preview
PDF
279Kb
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
Copyright:©2005 IFIP International Federation for Information Processing
Research Group:
Link to this item:http://purl.utwente.nl/publications/54796
Official URL:http://dx.doi.org/10.1007/11562436_9
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page

Metis ID: 229285