Marimba: A Tool for Verifying Properties of Hidden Markov Models
This provides a verification tool for HMMs, which is incremental as it builds on existing logics, aiding researchers and practitioners in fields like robotics who need formal assurance in model correctness.
The authors tackled the problem of verifying properties of Hidden Markov Models (HMMs) by developing Marimba, the first tool based on Zhang et al.'s POCTL* logics, and demonstrated its application by verifying properties in a human-robot interaction handover task using the robot Bert2.
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.