Back to University of Twente portal
Logic and model checking for hidden Markov models
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]](http://doc.utwente.nl/style/images/fileicons/application_pdf.png)
| 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 |
Show download statistics for this publication
Show download statistics for this publicationRepository Staff Only: item control page
Metis ID: 229285