### Abstract

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

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

}

*Logic and model checking for hidden Markov models*. AVACS Technical Report, no. 6, Transregional Collaborative Research Center 14 AVACS, Germany.

**Logic and model checking for hidden Markov models.** / Becker, B. (Editor); Zhang, Lijun; Hermanns, H.; Damm, Werner (Editor); Jansen, D.N.; Fränzle, Martin (Editor); Olderog, Ernst-Rüdiger (Editor); Podelski, Andreas (Editor); Wilhelm, R. (Editor).

Research output: Book/Report › Report › Professional

TY - BOOK

T1 - Logic and model checking for hidden Markov models

AU - Zhang, Lijun

AU - Hermanns, H.

AU - Jansen, D.N.

A2 - Becker, B.

A2 - Damm, Werner

A2 - Fränzle, Martin

A2 - Olderog, Ernst-Rüdiger

A2 - Podelski, Andreas

A2 - Wilhelm, R.

N1 - AVACS Technical Report No. 6

PY - 2005/7

Y1 - 2005/7

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

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

KW - METIS-248080

KW - EWI-1727

KW - IR-65545

M3 - Report

SN - 1860-9821

T3 - AVACS Technical Report

BT - Logic and model checking for hidden Markov models

PB - Transregional Collaborative Research Center 14 AVACS

CY - Germany

ER -