On Sep 11, 2026 I will give a talk on “Symbolic ω-automata with obligations” at HIGHLIGHTS 2026 in Vienna, Austria.

The talk is roughly based on this preprint, but will also present early work towards emptiness checking of automata with obligations and Büchi acceptance conditions. A proof-of-concept tool is available at https://github.com/lou1306/hoapp.

Abstract:

We consider symbolic omega-automata, i.e., automata over an alphabet of valuations of variables over possibly infinite domains. Typical approaches to retain information from past symbols rely on registers or memory cells, usually at the cost of rather intricate semantics.
We propose a slightly different approach based on obligations, i.e., assignment-like constructs attached to transitions, reminiscent of “next-state” constraints in SMV. Intuitively, whenever a transition with an obligation is taken, the obligation is evaluated on the current symbol and yields a constraint on the next symbol that the automaton will read. Thus, the effect of an obligation is ephemeral, compared to the persistent write operations in register automata.
We show the semantics of obligation automata with Emerson-Lei acceptance to be rather intuitive, when compared to, say, register automata. Although emptiness is undecidable in general we propose a semi-algorithm for emptiness, and discuss classes of obligation automata under which it is guaranteed to terminate. We can also generalise the semantics to support universal branching.
We also have a prototype implementation that supports several operations on these automata, by reusing Spot and IC3IA (an efficient IC3 model checker, used for emptiness checking).