Execution and monitoring of HOA automata with HOAX

TL;DR

The paper introduces Hoax, an open-source tool for executing and monitoring utomata in HOA format, capable of runtime verification and recognizing inconclusive prefixes, with formal foundations and practical evaluation.

Contribution

It presents a novel tool, Hoax, that enables execution and runtime monitoring of utomata with support for various acceptance conditions and recognition of ugly prefixes.

Findings

Hoax effectively monitors utomata in real-time.

It can recognize ugly prefixes when automata are not monitorable.

Performance comparison shows Hoax's practical utility against existing tools.

Abstract

We present a tool called Hoax for the execution of {\omega}-automata expressed in the popular HOA format. The tool leverages the notion of trap sets to enable runtime monitoring of any (non-parity) acceptance condition supported by the format. When the automaton is not monitorable, the tool may still be able to recognise so-called ugly prefixes, and determine that no further observation will ever lead to a conclusive verdict. The tool is open-source and highly configurable. We present its formal foundations, its design, and compare it against the trace analyser PyContract on a lock acquisition scenario.