Mungojerrie：线性时间目标的强化学习

强化学习在无系统先验知识的情况下合成控制器。在每个时间步给予一个奖励。控制器优化这些奖励的折扣和。应用这类算法需要设计奖励方案，这通常手动完成。设计者必须确保其意图被准确捕捉。这可能并不简单，且容易出错。相对于这种手动编程（类似于直接用汇编编程），另一种方式是以形式化语言指定目标并将其“编译”为奖励方案。Mungojerrie (https://plv.colorado.edu/mungojerrie/) 是一个用于在有限模型上测试 $\omega$-正则目标的奖励方案的工具。该工具包含强化学习算法和概率模型检测器。Mungojerrie支持PRISM中指定的模型和HOA中指定的 $\omega$-自动机。