SE PhD Prospectus Defense of Igor Cizelj

TITLE: Vehicle Control From Temporal Logic Specifications With Probabilistic Satisfaction Guarantees ABSTRACT: In this work, we propose to study the synthesis of control strategies for different vehicle models from rich specification languages by means of formal verification approaches. We consider complex vehicle models that involve systems of differential equations evolving over continuous domains and we wish to have a probabilistic guarantee that the behavior of a dynamic system, in the presence of sensing and actuation noise, satisfies a given specification. Recently, temporal logics have become increasingly popular for complex motion specifications. In order to use tools from formal verification for motion planning and control, most of the works using temporal logics as specification languages assume that the motion of the vehicle in the environment can be modeled as a finite system. However, we are interested in vehicle models whose dynamics are described by control systems with state and control variables evaluated over infinite domains. Even though recent works discuss the construction of a finite abstraction for stochastic continuous systems, the existing methods are either not applicable to vehicle dynamics or are computationally too expensive. To address this problem we will focus on the following research objectives: - Sampling-based techniques for vehicle abstraction and control from temporal logic specifications with probabilistic satisfaction guarantees: Efficient abstraction methods that exploit vehicle dynamics and are specification guided will be developed. The methods will consider sensor models as well, to produce closed-loop vehicle control strategies that maximize the probability of satisfying the specification. The work will bridge the gap between a low level sensory inputs and a high level temporal logic specifications. - Experimental setup for automatic vehicle deployment from temporal logic specifications: An experimental setup for vehicle deployment will be developed with a user interface for an environment and a specification input. A method for displaying the environment in which the vehicle will be deployed, under the synthesized control strategy, will be presented. To test the correctness of the vehicle motion a tracking system will be used. - Sensitivity analysis of temporal logic vehicle control with probabilistic satisfaction guarantees: Theoretical framework that enables user-vehicle negotiation process will be introduced. The framework will allow for a user to relax a constraint by changing the specification in order to increase the satisfaction probability, quickly and efficiently, by reusing the solution of the original problem. COMMITTEE: Advisor: Calin Belta, SE/ME; John Baillieul, SE/ME; Sean Andersson, SE/ME; Mac Schwager, SE/ME

NIS