Synthesis with Clairvoyance

Orna Kupferman, Dorsa Sadigh, and Sanjit A. Seshia. Synthesis with Clairvoyance. In Proceedings of the Haifa Verification Conference (HVC), December 2011.

Download

[pdf] 

Abstract

We consider the problem of automatically synthesizing, from a linear temporal logic (LTL) specification, a system that is guaranteed to satisfy the specification with respect to all environments. Algorithms for solving the synthesis problem reduce it to the solution of a game played between the system and its environment, in which the system and environment alternate between generating outputs and inputs respectively. Typically, the system is required to generate an output right after receiving the current input. If a solution to the game exists, the specification is said to be realizable.

In this paper, we consider the role of clairvoyance in synthesis, in which the system can "look into the future," basing its output upon future inputs. An infinite look-ahead transforms the realizability problem into a problem known as universal satisfiability. A thesis we explore in this paper is that the notion of clairvoyance is useful as a heuristic even in the general case of synthesis, when there is no lookahead. Specifically, we suggest a heuristic in which we search for strategies where the system and the environment try to force each other into hopeless states in the game --- states from which they cannot win, no matter how large the lookahead. The classification to hopeful and hopeless states is thus based on a modified notion of universal satisfiability where the output prefix is constrained. Our approach uses the automata for the specification in the process of classification into hopeful and hopeless states, and uses the structure of the automata in order to construct the game graph, but the important point is that the game itself is a reachability game. We demonstrate the efficiency of our approach with examples, and outline some directions for future work exploring the proposed approach.

BibTeX

@InProceedings{kupferman-hvc11,
  author = 	 {Orna Kupferman and Dorsa Sadigh and Sanjit A. Seshia},
  title = 	 {Synthesis with Clairvoyance},
  booktitle = {Proceedings of the Haifa Verification Conference (HVC)},
  month = {December},
  year = 	 {2011},
  abstract = {We consider the problem of automatically synthesizing, from 
a linear temporal logic (LTL) specification, a system 
that is guaranteed to satisfy the 
specification with respect to all environments.  
Algorithms for solving the synthesis problem reduce it to the solution 
of a game played between the system and its environment, in which 
the system and environment alternate between generating outputs and 
inputs respectively.  
Typically, the system is required to generate an output right after 
receiving the current input. If a solution to the game exists, the 
specification is said to be realizable. 
In this paper, we consider the role of clairvoyance in synthesis, in 
which the system can ``look into the future,'' basing its output upon future inputs.  
An infinite look-ahead transforms the realizability problem into  
a problem known as universal satisfiability.  
A thesis we explore in this paper is that the notion of clairvoyance 
is useful as a heuristic even in the general case of synthesis, when 
there is no lookahead. 
Specifically, we suggest a heuristic in which we search for strategies where 
the system and the environment try to force each other into  
hopeless states in the game --- states from which they cannot win, no 
matter how large the lookahead. 
The classification to hopeful 
and hopeless states is thus based on a modified notion of universal 
satisfiability where the output prefix is constrained. 
Our approach uses the automata for the specification in the 
process of classification into hopeful and hopeless states, and uses 
the structure of the automata in order to construct the game graph, 
but the important point is that  
the game itself is a reachability game. We demonstrate the 
efficiency of our approach with examples, and outline some 
directions for future work exploring the proposed approach.},
}