### 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.

Original language | Undefined |
---|---|

Place of Publication | Germany |

Publisher | Transregional Collaborative Research Center 14 AVACS |

Number of pages | 27 |

ISBN (Print) | 1860-9821 |

Publication status | Published - Jul 2005 |

### Publication series

Name | AVACS Technical Report |
---|---|

Publisher | Transregional Collaborative Research Center 14 AVACS |

No. | 6 |

ISSN (Print) | 1860-9821 |

### Keywords

- METIS-248080
- EWI-1727
- IR-65545

## Cite this

Becker, B. (Ed.), Zhang, L., Hermanns, H., Damm, W. (Ed.), Jansen, D. N., Fränzle, M. (Ed.), ... Wilhelm, R. (Ed.) (2005).

*Logic and model checking for hidden Markov models*. (AVACS Technical Report; No. 6). Germany: Transregional Collaborative Research Center 14 AVACS.