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 proceedingConference Contribution (Conference Proceeding)

252 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 languageEnglish
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
PublisherSpringer Verlag
Pages201-206
Number of pages6
Volume9364
ISBN (Print)9783319249520
DOIs
Publication statusPublished - 22 Nov 2015
Event13th International Symposium on Automated Technology for Verification and Analysis, ATVA 2015 - Shanghai, China
Duration: 12 Oct 201515 Oct 2015

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9364
ISSN (Print)03029743
ISSN (Electronic)16113349

Conference

Conference13th International Symposium on Automated Technology for Verification and Analysis, ATVA 2015
CountryChina
CityShanghai
Period12/10/1515/10/15

Fingerprint Dive into the research topics of 'Marimba: A tool for verifying properties of hidden markov models'. Together they form a unique fingerprint.

Cite this