Certifying Inexpressibility
Orna Kupferman, Salomon Sickert

TL;DR
This paper introduces a game-based framework for certifying inexpressibility of languages by automata, providing simple certificates and handling various automata classes including deterministic and restricted ones.
Contribution
It presents a game-theoretic approach to certify inexpressibility and separation, applicable to multiple automata classes, and offers methods for automata approximation.
Findings
Winning strategies serve as certificates of inexpressibility.
Framework applies to all deterministic automata classes, including weak automata.
Can be used for automata-based separation and approximation tasks.
Abstract
Different classes of automata on infinite words have different expressive power. Deciding whether a given language can be expressed by an automaton of a desired class can be reduced to deciding a game between Prover and Refuter: in each turn of the game, Refuter provides a letter in , and Prover responds with an annotation of the current state of the run (for example, in the case of B\"uchi automata, whether the state is accepting or rejecting, and in the case of parity automata, what the color of the state is). Prover wins if the sequence of annotations she generates is correct: it is an accepting run iff the word generated by Refuter is in . We show how a winning strategy for Refuter can serve as a simple and easy-to-understand certificate to inexpressibility, and how it induces additional forms of certificates. Our framework handles all classes…
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.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
