Multi agent control with LTL specifications and abstraction with input memories

Sammanfattning: Formal controller synthesis methods with temporal logic specications tryto guarantee the correctness of given specications with a system that mighthave complex behaviour. Most often, discrete abstractions of a continuoussystem are used in order to reduce the size of the problem. If a behaviouralrelationship between the system and its abstraction is met, then a valid controllerfor the abstraction will be valid as well for the system. The nitenessof the abstraction allows us to use computer science tools to synthesize anite state controller (graphs search and xed point algorithms, temporallogics). These methods are automatic (the controller synthesis can be createdautomatically from the specications) and oine (the controller is createdbeforehand).In this work, we investigate a system with a state extended by memoriesof the last inputs. These memories are used to compute the reachable sets,this counteract the loss of information from a partial observation of the state.The nal abstraction is obtained by a discretization of the resulting statespace, and expressed as an Augmented Finite Transition System (AFTS).This AFTS extends the classical Finite Transition System denition with aprogress set that identies terminating local control strategies. As the AFTSis alternatingly simulated by the extended system, a controller solution of theproblem for the AFTS is a solution for the extended system. Specicationsof the controller are given in Linear Temporal Logic formula (LTL). Theproduct of the non deterministic AFTS and the Buchi automaton of the LTLspecication is dened. An algorithm that can nd non-blocking controlstrategy for the AFTS is then used to nd a nite state controller.This controller synthesis method with Linear Temporal Logic specicationshas been successfully used and tested on single and multiple quadricoptersscenarios in the Smart Mobility Lab of KTH.