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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
