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

    15 Citations (Scopus)
    44 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
    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
    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.