.png){kind=icon}
.png){kind=icon}
Return
Synthesis With Guided Environments
.png){kind=icon}
OA
AI
O
O
DOI：10.1109/tse.2026.3686926.png)
.png){kind=icon}
Original request for help.png){kind=icon}
Share.png){kind=icon}
Save
Abstract
En 中文
In the synthesis problem, we are given a specification, and we automatically generate a system that satisfies the specification in all environments. We introduce and study <italic xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">synthesis with guided environments</i> (SGE, for short), where the system may harness the knowledge and computational power of the environment during the interaction. The underlying idea in SGE is that in many real-life applications, in particular when the system serves or directs the environment, it is in the environment’s interest that the specification is satisfied; hence, it is reasonable to consider satisfaction of the specification only in environments that follow the system’s guidance. Thus, while the environment is still hostile, in the sense that the system should satisfy the specification no matter how the environment assigns values to the input signals, in SGE the system assigns values to some output signals and guides the environment via <italic xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">programs</i> how to assign values to other output signals. A key issue is that these assignments may depend on input signals that are hidden from the system but are known to the environment. SGE is thus particularly useful in settings where the system has partial visibility. In software systems, this corresponds to settings that involve hidden user intents, client-local states, or private service policies. We solve the problem of SGE, show its superiority with respect to traditional synthesis, and study theoretical aspects of SGE, like the complexity (memory and domain) of programs used by the system, SGE for branching-time specifications, and the connection of SGE to synthesis of (possibly distributed) systems with partial visibility.
Keywords:
Synthesis
partial visibility
temporal logic, automata
Journal
IF:
5.6
Papers:
2.8K
Citations:
1.1W
Organization
Cited Papers