FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Heuristic-Based GR(1) Assumptions Refinement

Author: Davide Giacomo Cavezza

Paper Information

Title:Heuristic-Based GR(1) Assumptions Refinement
Authors:Davide Giacomo Cavezza
Proceedings:DS-FM Students papers
Editor: Fatiha Zaidi
Keywords:assumptions refinement, controller synthesis, generalized reactivity, heuristic search
Abstract:

ABSTRACT. In order to synthesize automatically a controller satisfying a specification given in GR(1) (a subset of linear temporal logic), the environment, where the controller is expected to operate, needs to be characterized by a sufficient set of GR(1) assumptions. Assumptions refinement procedures identify alternative sets of assumptions that make controller synthesis possible. However, since assumptions spaces are intractably large, techniques to explore a subset of them in a guided fashion are needed. In particular, it is important to identify weakest assumptions refinements to avoid overconstraining the environments and hence deeming the controller to be inadequate. The objective of my research is to devise a heuristic search approach that uses estimates of goodness of explored assumptions to direct the search towards better solutions. The work involves defining computable metrics that capture quality features of assumptions (such as their weakness), and automated ways to select a good subset of refinements in the search procedure.

Pages:4
Talk:Jul 14 11:45 (Session 95B: DS-FM invited talk: Sylvain Conchon)
Paper: