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

    13 Citations (Scopus)
    32 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.
    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). / Logic and model checking for hidden Markov models. Germany : Transregional Collaborative Research Center 14 AVACS, 2005. 27 p. (AVACS Technical Report; 6).
    @book{7582f59f5286462da104106312f8e7b8,
    title = "Logic and model checking for hidden Markov models",
    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.",
    keywords = "METIS-248080, EWI-1727, IR-65545",
    author = "Lijun Zhang and H. Hermanns and D.N. Jansen",
    editor = "B. Becker and Werner Damm and Martin Fr{\"a}nzle and Ernst-R{\"u}diger Olderog and Andreas Podelski and R. Wilhelm",
    note = "AVACS Technical Report No. 6",
    year = "2005",
    month = "7",
    language = "Undefined",
    isbn = "1860-9821",
    series = "AVACS Technical Report",
    publisher = "Transregional Collaborative Research Center 14 AVACS",
    number = "6",

    }

    Becker, B (ed.), Zhang, L, Hermanns, H, Damm, W (ed.), Jansen, DN, Fränzle, M (ed.), Olderog, E-R (ed.), Podelski, A (ed.) & Wilhelm, R (ed.) 2005, 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).

    Germany : Transregional Collaborative Research Center 14 AVACS, 2005. 27 p. (AVACS Technical Report; No. 6).

    Research output: Book/ReportReportProfessional

    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 -

    Becker B, (ed.), Zhang L, Hermanns H, Damm W, (ed.), Jansen DN, Fränzle M, (ed.) et al. Logic and model checking for hidden Markov models. Germany: Transregional Collaborative Research Center 14 AVACS, 2005. 27 p. (AVACS Technical Report; 6).