Coverability: Realizability Lower Bounds

TL;DR

This paper introduces the concept of temporal coverability for realizability and synthesis, providing methods to automatically generate systems that cover specified languages while addressing correctness and environment assumptions.

Contribution

It presents a counting-based automaton approach for coverability, extending to specifications with correctness criteria, and offers an alternative to traditional synthesis methods.

Findings

Counting argument enables system construction for coverability.

Preconditions for systems satisfying additional specifications are established.

Approach addresses issues with environment assumptions and guarantees in synthesis.

Abstract

We introduce the problem of temporal coverability for realizability and synthesis. Namely, given a language of words that must be covered by a produced system, how to automatically produce such a system. We consider the case of coverability with no further specifications, where we have to show that the nondeterminism of the produced system is sufficient to produce all the words required in the output language. We show a counting argument on a deterministic automaton representing the language to be covered that allows to produce such a system. We then turn to the case of coverability with additional specification and give a precondition for the existence of a system that produces all required words and at the same time produces only computations satisfying the additional correctness criterion. We combine our counting argument on the deterministic automaton for the language to be covered with a ranking on the deterministic B\"uchi automaton for the correctness criterion. One of the major issues with practical realizability is the interaction between environment assumptions and system guarantees. In many cases, synthesis produces systems that are vacuous and concentrate on forcing the environment to falsify its assumptions instead of fulfilling their guarantees. Coverability offers an alternative approach to tackle this problem.