Marimba: A tool for verifying properties of hidden markov models

Noé Hernández; Kerstin Eder; Evgeni Magid; Jesús Savage; David A. Rosenblueth

doi:10.1007/978-3-319-24953-7_14

Marimba: A tool for verifying properties of hidden markov models

Noé Hernández^*, Kerstin Eder, Evgeni Magid, Jesús Savage, David A. Rosenblueth

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference Contribution (Conference Proceeding)

1 Citation (Scopus)

350 Downloads (Pure)

Abstract

The formal verification of properties of Hidden Markov Models (HMMs) is highly desirable for gaining confidence in the correctness of the model and the corresponding system. A significant step towards HMM verification was the development by Zhang et al. of a family of logics for verifying HMMs, called POCTL*, and its model checking algorithm. As far as we know, the verification tool we present here is the first one based on Zhang et al.’s approach. As an example of its effective application, we verify properties of a handover task in the context of human-robot interaction. Our tool was implemented in Haskell, and the experimental evaluation was performed using the humanoid robot Bert2.

Original language	English
Title of host publication	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Publisher	Springer Verlag
Pages	201-206
Number of pages	6
Volume	9364
ISBN (Print)	9783319249520
DOIs	https://doi.org/10.1007/978-3-319-24953-7_14
Publication status	Published - 22 Nov 2015
Event	13th International Symposium on Automated Technology for Verification and Analysis, ATVA 2015 - Shanghai, China Duration: 12 Oct 2015 → 15 Oct 2015

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	9364
ISSN (Print)	03029743
ISSN (Electronic)	16113349

Conference

Conference	13th International Symposium on Automated Technology for Verification and Analysis, ATVA 2015
Country/Territory	China
City	Shanghai
Period	12/10/15 → 15/10/15

Access to Document

10.1007/978-3-319-24953-7_14

Kerstin Eder - Marimba - A Tool for Verifying Properties of Hidden Markov Models
This is the author accepted manuscript (AAM). The final published version (version of record) is available online via Springer at 10.1007/978-3-319-24953-7_14.
Accepted author manuscript, 289 KB

Handle.net

Persistent link

Cite this

Hernández, N., Eder, K., Magid, E., Savage, J., & Rosenblueth, D. A. (2015). Marimba: A tool for verifying properties of hidden markov models. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9364, pp. 201-206). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9364). Springer Verlag. https://doi.org/10.1007/978-3-319-24953-7_14

Hernández, Noé ; Eder, Kerstin ; Magid, Evgeni et al. / Marimba : A tool for verifying properties of hidden markov models. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 9364 Springer Verlag, 2015. pp. 201-206 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{1a013892a4e64157a3bd49ecaad0a479,

title = "Marimba: A tool for verifying properties of hidden markov models",

abstract = "The formal verification of properties of Hidden Markov Models (HMMs) is highly desirable for gaining confidence in the correctness of the model and the corresponding system. A significant step towards HMM verification was the development by Zhang et al. of a family of logics for verifying HMMs, called POCTL*, and its model checking algorithm. As far as we know, the verification tool we present here is the first one based on Zhang et al.{\textquoteright}s approach. As an example of its effective application, we verify properties of a handover task in the context of human-robot interaction. Our tool was implemented in Haskell, and the experimental evaluation was performed using the humanoid robot Bert2.",

author = "No{\'e} Hern{\'a}ndez and Kerstin Eder and Evgeni Magid and Jes{\'u}s Savage and Rosenblueth, {David A.}",

year = "2015",

month = nov,

day = "22",

doi = "10.1007/978-3-319-24953-7_14",

language = "English",

isbn = "9783319249520",

volume = "9364",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "201--206",

booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

address = "Germany",

note = "13th International Symposium on Automated Technology for Verification and Analysis, ATVA 2015 ; Conference date: 12-10-2015 Through 15-10-2015",

}

Hernández, N, Eder, K, Magid, E, Savage, J & Rosenblueth, DA 2015, Marimba: A tool for verifying properties of hidden markov models. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). vol. 9364, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9364, Springer Verlag, pp. 201-206, 13th International Symposium on Automated Technology for Verification and Analysis, ATVA 2015, Shanghai, China, 12/10/15. https://doi.org/10.1007/978-3-319-24953-7_14

Marimba: A tool for verifying properties of hidden markov models. / Hernández, Noé; Eder, Kerstin; Magid, Evgeni et al.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 9364 Springer Verlag, 2015. p. 201-206 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9364).

Research output: Chapter in Book/Report/Conference proceeding › Conference Contribution (Conference Proceeding)

TY - GEN

T1 - Marimba

T2 - 13th International Symposium on Automated Technology for Verification and Analysis, ATVA 2015

AU - Hernández, Noé

AU - Eder, Kerstin

AU - Magid, Evgeni

AU - Savage, Jesús

AU - Rosenblueth, David A.

PY - 2015/11/22

Y1 - 2015/11/22

N2 - The formal verification of properties of Hidden Markov Models (HMMs) is highly desirable for gaining confidence in the correctness of the model and the corresponding system. A significant step towards HMM verification was the development by Zhang et al. of a family of logics for verifying HMMs, called POCTL*, and its model checking algorithm. As far as we know, the verification tool we present here is the first one based on Zhang et al.’s approach. As an example of its effective application, we verify properties of a handover task in the context of human-robot interaction. Our tool was implemented in Haskell, and the experimental evaluation was performed using the humanoid robot Bert2.

AB - The formal verification of properties of Hidden Markov Models (HMMs) is highly desirable for gaining confidence in the correctness of the model and the corresponding system. A significant step towards HMM verification was the development by Zhang et al. of a family of logics for verifying HMMs, called POCTL*, and its model checking algorithm. As far as we know, the verification tool we present here is the first one based on Zhang et al.’s approach. As an example of its effective application, we verify properties of a handover task in the context of human-robot interaction. Our tool was implemented in Haskell, and the experimental evaluation was performed using the humanoid robot Bert2.

UR - http://www.scopus.com/inward/record.url?scp=84951731312&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-24953-7_14

DO - 10.1007/978-3-319-24953-7_14

M3 - Conference Contribution (Conference Proceeding)

AN - SCOPUS:84951731312

SN - 9783319249520

VL - 9364

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 201

EP - 206

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

PB - Springer Verlag

Y2 - 12 October 2015 through 15 October 2015

ER -

Hernández N, Eder K, Magid E, Savage J, Rosenblueth DA. Marimba: A tool for verifying properties of hidden markov models. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 9364. Springer Verlag. 2015. p. 201-206. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-24953-7_14

Marimba: A tool for verifying properties of hidden markov models

Abstract

Publication series

Conference

Access to Document

Handle.net

Other files and links

Fingerprint

Trustworthy Robotic Assistants

Cite this

Marimba: A tool for verifying properties of hidden markov models

Abstract

Publication series

Conference

Access to Document

Handle.net

Other files and links

Fingerprint

Projects

Trustworthy Robotic Assistants

Cite this