HOA 自动机的执行与监控——HOAX

我们提出了一个名为 Hoax 的工具，用于执行以流行 HOA 格式表示的 $\omega$-automata。该工具利用陷阱集（trap sets）的概念，以支持格式所支持的任何 (非 parity) 接受条件实现运行时监控。当自动机不可监控时，该工具仍可能识别所谓的丑陌前缀（ugly prefixes），并确定无进一步观察将导致 conclusive verdict。该工具开源且高度可配置。我们呈现其形式化基础、设计，并将其与针对锁获取情景的 trace analyser PyContract 进行比较。