Marimba: A Tool for Verifying Properties of Hidden Markov Models

TL;DR

Marimba is a novel verification tool for Hidden Markov Models that implements Zhang et al.'s POCTL* logic, enabling formal property verification with practical application demonstrated in human-robot interaction.

Contribution

This paper introduces the first verification tool based on Zhang et al.'s POCTL* logic for HMMs, implemented in Haskell and validated through a human-robot interaction case study.

Findings

Successfully verified properties of HMMs in a human-robot interaction scenario

First implementation of Zhang et al.'s HMM verification approach

Demonstrated practical applicability with experimental evaluation on humanoid robot Bert2

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.