Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Symbolic ω-automata with obligations

Luca Di Stefano

TL;DR

This paper introduces obligation automata, a finite-state model for ω-automata with infinite alphabets that attach assignment-like obligations to transitions, enabling expressive yet tractable semantics. It formalizes existential and universal branching with Emerson-Lei acceptance, showing that obligations extend ω-regular languages and can express certain infinite-state behaviors beyond traditional ω-automata. To enable practical use, the authors present HOApp, a dialect of HOA with typeable variable predicates, LTL-based guarantees, and assume constructs, along with a prototype tool that supports automata product, LTL translation, and emptiness checking via SMT/model checking. The work also provides a lowering/inflation path to HOA and demonstrates applicability through an arbiter example, outlining future directions for complementation, richer theories, and synthesis applications.

Abstract

Extensions of ω-automata to infinite alphabets typically rely on symbolic guards to keep the transition relation finite, and on registers or memory cells to preserve information from past symbols. Symbolic transitions alone are ill-suited to act on this information, and register automata have intricate formal semantics and issues with tractability. We propose a slightly different approach based on obligations, i.e., assignment-like constructs attached to transitions. Whenever a transition with an obligation is taken, the obligation is evaluated against the current symbol and yields a constraint on the next symbol that the automaton will read. We formalize obligation automata with existential and universal branching and Emerson-Lei acceptance conditions, which subsume classic families such as Büchi, Rabin, Strett, and parity automata. We show that these automata recognise a strict superset of ω-regular languages. To illustrate the practicality of our proposal, we also introduce a machine-readable format to express obligation automata and describe a tool implementing several operations over them, including automata product and emptiness checking.

Symbolic ω-automata with obligations

TL;DR

This paper introduces obligation automata, a finite-state model for ω-automata with infinite alphabets that attach assignment-like obligations to transitions, enabling expressive yet tractable semantics. It formalizes existential and universal branching with Emerson-Lei acceptance, showing that obligations extend ω-regular languages and can express certain infinite-state behaviors beyond traditional ω-automata. To enable practical use, the authors present HOApp, a dialect of HOA with typeable variable predicates, LTL-based guarantees, and assume constructs, along with a prototype tool that supports automata product, LTL translation, and emptiness checking via SMT/model checking. The work also provides a lowering/inflation path to HOA and demonstrates applicability through an arbiter example, outlining future directions for complementation, richer theories, and synthesis applications.

Abstract

Extensions of ω-automata to infinite alphabets typically rely on symbolic guards to keep the transition relation finite, and on registers or memory cells to preserve information from past symbols. Symbolic transitions alone are ill-suited to act on this information, and register automata have intricate formal semantics and issues with tractability. We propose a slightly different approach based on obligations, i.e., assignment-like constructs attached to transitions. Whenever a transition with an obligation is taken, the obligation is evaluated against the current symbol and yields a constraint on the next symbol that the automaton will read. We formalize obligation automata with existential and universal branching and Emerson-Lei acceptance conditions, which subsume classic families such as Büchi, Rabin, Strett, and parity automata. We show that these automata recognise a strict superset of ω-regular languages. To illustrate the practicality of our proposal, we also introduce a machine-readable format to express obligation automata and describe a tool implementing several operations over them, including automata product and emptiness checking.

Paper Structure

This paper contains 11 sections, 10 equations, 7 figures, 3 tables.

Table of Contents

  1. Introduction
  2. Obligation automata
  3. The HOApp format
  4. Overview of HOA
  5. Syntactic extensions to HOA
  6. Typing rules
  7. Semantics
  8. Example: A simple arbiter
  9. The hoapp tool
  10. Conclusion
  11. Negative obligations

Figures (7)

  • Figure 1: Recognising the language $\mathcal{L}$ of a repeatedly-incrementing counter.
  • Figure 2: Automata for a language of non-repeating values of $x$.
  • Figure 3: HOA description of a Büchi automaton for $G\, x$.
  • Figure 4: Graphical representation of the automaton from Listing \ref{['ex:arbiter']}.
  • Figure 5: Overview of the capabilities of the hoapp tool.
  • ...and 2 more figures

Theorems & Definitions (3)

  • proof
  • proof
  • proof