Synthesis from Knowledge-Based Specifications

TL;DR

This paper addresses the challenge of synthesizing reactive systems from knowledge-based specifications under incomplete information, demonstrating that the complexity remains comparable to the complete information case.

Contribution

It introduces a method for synthesis with incomplete information using knowledge and time logic, establishing complexity equivalence with complete information synthesis.

Findings

Synthesis with incomplete information has the same worst-case complexity as complete information.

Knowledge-based specifications effectively model uncertainty in reactive system synthesis.

The approach enables synthesis when the environment's attributes are only partially observable.

Abstract

In program synthesis, we transform a specification into a program that is guaranteed to satisfy the specification. In synthesis of reactive systems, the environment in which the program operates may behave nondeterministically, e.g., by generating different sequences of inputs in different runs of the system. To satisfy the specification, the program needs to act so that the specification holds in every computation generated by its interaction with the environment. Often, the program cannot observe all attributes of its environment. In this case, we should transform a specification into a program whose behavior depends only on the observable history of the computation. This is called synthesis with incomplete information. In such a setting, it is desirable to have a knowledge-based specification, which can refer to the uncertainty the program has about the environment's behavior. In this work we solve the problem of synthesis with incomplete information with respect to specifications in the logic of knowledge and time. We show that the problem has the same worst-case complexity as synthesis with complete information.