Funding agency: Natural Sciences and Engineering Research Council of Canada
Yves Lespérance, Department of Electrical Engineering and Computer Science, York University
Duration: 5 years (2015 -- 2020)
The focus is not primarily on planning, where one synthesizes a plan to achieve a goal from a set of primitive actions. Instead, we consider problems such as customization/supervision, where we already have an agent or system and we want to constrain its behaviour to meet a set of specifications, and composition/orchestration, where we have a set of available agents and we want to compose them to obtain a new system that meets satisfies some temporally extended goal.
A major advance in our recent work has been the identification of an important class of action theories for which verification of temporal properties is decidable. In the project, we will further develop this bounded action theories framework to accomodate more realistic models of agents. We will also develop techniques and tools for doing verification and synthesis for such bounded theories.
We will apply these methods to agent supervision, a form of customization where the agent's behaviour is constrained to satisfy a specification. Since some actions may be uncontrollable, it may not be possible to restrict the agent to perform exactly the set of action sequences that satisfy the specification. Our approach finds the maximally permissive supervisor that gives as much flexibility/autonomy to the agent as possible while ensuring that it complies with the specification. In the project, we will generalize our agent supervision framework to handle complex hierarchical/modular systems.
We will also continue our work on fixpoint approximation techniques for agent verification and synthesis. These techniques are incomplete, but can be used on general infinite state systems.
back to [Yves Lespérance]