这是 lbt 命令，可以使用我们的多个免费在线工作站之一在 OnWorks 免费托管服务提供商中运行，例如 Ubuntu Online、Fedora Online、Windows 在线模拟器或 MAC OS 在线模拟器
程序：
您的姓名
lbt - LTL 到 Büchi 翻译器
概要
LBT < 公式.txt > 自动机.txt
LBT2点 < 自动机.txt > 自动机.dot
商品描述
本手册页简要记录了 LBT 和 LBT2点 命令。 这个手册页是
为 Debian GNU/Linux 发行版编写，因为原始程序没有
手册页。 相反，它有 HTML 格式的文档； 见下文。
LBT 是将线性时序逻辑 (LTL) 公式转换为相应的过滤器
广义 Büchi 自动机。 翻译基于 Gerth, Peled 的算法
和 Vardi 出现在 PSTV'95 上， 简易 即时 自动 验证 of 线性
颞 逻辑. 几乎没有实现任何优化，生成的自动机是
通常比必要的大。 但另一方面，它应该始终是正确的。
过滤器 LBT2点 可用于翻译 Büchi 自动机 LBT 输出格式为
用于可视化的 GraphViz 格式。
例
回音 G p0 | LBT | LBT2点 | 点点 -
使用 onworks.net 服务在线使用 lbt
