Vacuity in synthesis

Roderick Bloem, Hana Chockler, Masoud Ebrahimi, Ofer Strichman*

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

2 Citations (Scopus)


In reactive synthesis, one begins with a temporal specification φ, and automatically synthesizes a system M such that M⊧ φ. As many systems can satisfy a given specification, it is natural to seek ways to force the synthesis tool to synthesize systems that are of a higher quality, in some well-defined sense. In this article we focus on a well-known measure of the way in which a system satisfies its specification, namely vacuity. Our conjecture is that if the synthesized system M satisfies φnon-vacuously, then M is likely to be closer to the user’s intent, because it satisfies φ in a more “meaningful” way. Narrowing the gap between the formal specification and the designer’s intent in this way, automatically, is the topic of this article. Specifically, we propose a bounded synthesis method for achieving this goal. The notion of vacuity as defined in the context of model checking, however, is not necessarily refined enough for the purpose of synthesis. Hence, even when the synthesized system is technically non-vacuous, there are yet more interesting (equivalently, less vacuous) systems, and we would like to be able to synthesize them. To that end, we cope with the problem of synthesizing a system that is as non-vacuous as possible, given that the set of interesting behaviours with respect to a given specification induce a partial order on transition systems. On the theoretical side we show examples of specifications for which there is a single maximal element in the partial order (i.e., the most interesting system), a set of equivalent maximal elements, or a number of incomparable maximal elements. We also show examples of specifications that induce infinite chains of increasingly interesting systems. These results have implications on how non-vacuous the synthesized system can be. We implemented the new procedure in our synthesis tool PARTY. For this purpose we added to it the capability to synthesize a system based on a property which is a conjunction of universal and existential LTL formulas.

Original languageEnglish
Pages (from-to)473-495
Number of pages23
Issue number3
Publication statusPublished - Sept 2021


  • Bounded synthesis
  • Reactive synthesis
  • Vacuity


Dive into the research topics of 'Vacuity in synthesis'. Together they form a unique fingerprint.

Cite this