SitCalc Abstractions for Program Synthesis
This page contains all relevant information about “Situation Calculus Temporally Lifted Abstractions for Program Synthesis,” by Giuseppe De Giacomo, Yves Lespérance and Matteo Mancanelli.
Links
Here you can find some useful links:
[]
[short paper]
[full paper]
[poster]
We address a program synthesis task where one wants to automatically synthesize a controller that operates on data structures to accomplish an objective. We develop a framework that allows a programmer to provide an abstract description of how the data structure should evolve to satisfy the objectives and then derive a concrete program from that abstraction. The framework is based on the nondeterministic situation calculus, extended with LTL trace constraints. We propose a notion of temporally lifted abstraction to address the scenario in which we have a single high-level action theory/model with incomplete information and nondeterministic actions and a concrete action theory with several models and complete information. LTL formulas are used to specify the temporally extended goals as well as assumed trace constraints on the data structures used that hold at the concrete level. We show show that if we have such a temporally lifted abstraction and the agent has a strategy to achieve a LTL goal under some trace constraints at the abstract level, then there exists a refinement of the strategy to achieve the refinement of the goal at the concrete level. If the abstract theory is propositional, we can try to obtain such a strategy through LTL synthesis. We present several examples where we use our framework to solve problems involving data structures. We discuss the relationship of our approach to work on generalized planning.
Contacts
Giuseppe De Giacomo
University of Oxford, Oxford, UK
Email: giuseppe.degiacomo [at] cs.ox.ac.uk
[website]
Matteo Mancanelli
Sapienza University, Rome, Italy
Email: mancanelli [at] diag.uniroma1.it