@inproceedings{2340f74461c4420f8b50f8d78e144c08,
title = "Logic and model checking for hidden Markov models",
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.",
keywords = "METIS-229285, EWI-1424, IR-54796",
author = "Lijun Zhang and H. Hermanns and D.N. Jansen",
note = "ZHJ05 ; 25th IFIP WG 6.1 international conference, Taipei, Taiwan ; Conference date: 02-10-2005 Through 05-10-2005",
year = "2005",
month = oct,
doi = "10.1007/11562436_9",
language = "Undefined",
isbn = "3-540-29189-X",
series = "Lecture notes in computer science",
publisher = "Springer",
number = "XII",
pages = "98--112",
editor = "F. Wang",
booktitle = "Formal techniques for networked and distributed systems, FORTE",
address = "Germany",
}