Marimba：验证隐马尔可夫模型性质的工具
计算机科学中的逻辑
2015-10-29 v2 机器人学
摘要
对隐马尔可夫模型（HMMs）的性质进行形式化验证，对于确信模型及相应系统的正确性非常必要。Zhang 等人开发的一系列用于验证 HMM 的逻辑，称为 POCTL*，及其模型检验算法，是迈向 HMM 验证的重要一步。据我们所知，我们在此展示的验证工具是基于 Zhang 等人方法的第一个工具。作为其有效应用的一个例子，我们验证了人机交互背景下交接任务的性质。我们的工具使用 Haskell 实现，实验评估则使用人形机器人 Bert2 进行。
引用
@article{arxiv.1507.05597,
title = {Marimba: A Tool for Verifying Properties of Hidden Markov Models},
author = {Noe Hernandez and Kerstin Eder and Evgeni Magid and Jesus Savage and David A. Rosenblueth},
journal= {arXiv preprint arXiv:1507.05597},
year = {2015}
}
备注
Tool paper accepted in the 13th International Symposium on Automated Technology for Verification and Analysis (ATVA 2015)