SitCalc Abstractions for Program Synthesis
Questa pagina contiene tutte le informazioni su “Situation Calculus Temporally Lifted Abstractions for Program Synthesis”, di Giuseppe De Giacomo, Yves Lespérance e Matteo Mancanelli.
Link
Qui trovi alcuni link utili:
[]
[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.
Contatti
Giuseppe De Giacomo
University of Oxford, Oxford, UK
Email: giuseppe.degiacomo [at] cs.ox.ac.uk
Yves Lespérance
York University, Toronto, ON, Canada
Email: lesperan [at] eecs.yorku.ca
Matteo Mancanelli
Sapienza University, Rome, Italy
Email: mancanelli [at] diag.uniroma1.it