Logic and model checking for hidden Markov models

Lijun Zhang, H. Hermanns, D.N. Jansen

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

100 Downloads (Pure)

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 languageUndefined
Title of host publicationFormal techniques for networked and distributed systems, FORTE
EditorsF. Wang
Place of PublicationBerlin, Germany
PublisherSpringer
Pages98-112
Number of pages15
ISBN (Print)3-540-29189-X
DOIs
Publication statusPublished - Oct 2005
Event25th IFIP WG 6.1 international conference, Taipei, Taiwan: Formal techniques for networked and distributed systems, FORTE 2005 - Berlin
Duration: 2 Oct 20055 Oct 2005

Publication series

NameLecture notes in computer science
PublisherSpringer-Verlag
NumberXII
Volume3731
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference25th IFIP WG 6.1 international conference, Taipei, Taiwan
CityBerlin
Period2/10/055/10/05

Keywords

  • METIS-229285
  • EWI-1424
  • IR-54796

Cite this