@book{7582f59f5286462da104106312f8e7b8,
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-248080, EWI-1727, IR-65545",
author = "Lijun Zhang and H. Hermanns and D.N. Jansen",
editor = "B. Becker and Werner Damm and Martin Fr{\"a}nzle and Ernst-R{\"u}diger Olderog and Andreas Podelski and R. Wilhelm",
note = "AVACS Technical Report No. 6",
year = "2005",
month = jul,
language = "Undefined",
isbn = "1860-9821",
series = "AVACS Technical Report",
publisher = "Transregional Collaborative Research Center 14 AVACS",
number = "6",
}