LTL3BA：改进版 LTL2BA 的 LTL 公式到 Büchi 自动机的翻译工具（开源）

简介：
LTL3BA是一款用于将线性时序逻辑(LTL)公式转换为Büchi自动机的开源工具，它是对LTL2BA的增强版本。 LTL3BA 是一个将 LTL 公式转换为 Büchi 自动机的工具，它基于由 Denis Oddoux 和 Paul Gastin 编写的流行工具 LTL2BA。相较于后者，LTL3BA 在性能上有所提升。相关改进在论文《T. Babiak、M. Křetínský、V. Řehák 和 J. Strejček：LTL to Büchi Automata Translation: Fast and More Deterministic》中有详细描述，该文发表于 TACAS 2012 年会议的 LNCS 第 7214 卷，第 95 至 109 页。从 LTL3BA 的版本 1.1.0 开始支持以河内欧米茄自动机 (HOA) 格式输出。关于 HOA 更多的信息可以在相关资料中找到。为了编译 LTL3BA，需要使用 BuDDy 库。