Logic and model checking for hidden Markov models

B. Becker (Editor), Lijun Zhang, H. Hermanns, Werner Damm (Editor), D.N. Jansen, Martin Fränzle (Editor), Ernst-Rüdiger Olderog (Editor), Andreas Podelski (Editor), R. Wilhelm (Editor)

    Research output: Book/ReportReportProfessional

    16 Citations (Scopus)
    60 Downloads (Pure)


    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
    Place of PublicationGermany
    PublisherTransregional Collaborative Research Center 14 AVACS
    Number of pages27
    ISBN (Print)1860-9821
    Publication statusPublished - Jul 2005

    Publication series

    NameAVACS Technical Report
    PublisherTransregional Collaborative Research Center 14 AVACS
    ISSN (Print)1860-9821


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

    Cite this