Execution and monitoring of HOA automata with HOAX

Fuente: arXiv
Saved in:
Bibliographic Details
Main Author: Di Stefano, Luca
Format: Preprint
Published: 2025
Subjects:
Online Access:
Tags: Add Tag
No Tags, Be the first to tag this record!
_version_ 1866911298503049216
author Di Stefano, Luca
author_facet Di Stefano, Luca
contents We present a tool called Hoax for the execution of ω-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.
format Preprint
id arxiv_https___arxiv_org_abs_2507_11126
institution arXiv
publishDate 2025
record_format arxiv
spellingShingle Execution and monitoring of HOA automata with HOAX
Di Stefano, Luca
Logic in Computer Science
Formal Languages and Automata Theory
We present a tool called Hoax for the execution of ω-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.
title Execution and monitoring of HOA automata with HOAX
topic Logic in Computer Science
Formal Languages and Automata Theory
url https://arxiv.org/abs/2507.11126