Multi agent control with LTL specifications and abstraction with input memories

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.Formella metoder för att syntetisera regulatorer med temporal logiks specifikationer försöker att garantera att den givna specifikationen uppfylls avett system som kan ha komplexa beteenden. Oftast används diskreta abstraktionerav kontinuerliga system för att minska problemets storlek. Om enbeteende-relation mellan systemet och dess abstraktion är uppfylld så är en regulatorsom är giltig för abstraktionen också giltig för systemet. Ändlighetenav abstraktionen tillåter oss att använda datavetenskapliga verktyg för attsyntetisera en ändlig tillståndsregulator (grafsökning och fastpunktsalgorithmer,temporal logik). Dessa metoder är automatiska (regulator syntetiseringenkan göras automatiskt från specifikationen) och offline (regulatorn skapasi förväg).I det här arbetet undersöker vi ett system med utvidgat tillstånd somhar minnen som sista indata. Dessa minnen används för att beräkna seten avnåbara tillstånd. Detta motverkar förlusten av information som kan uppstå pågrund av en partiell observation av tillståndet. Den slutgiltiga abstraktionenfås genom en diskretisering av det resulterande tillståndsrummet och uttryckssom ett Utökat Ändligt Övergångs System (Augmented Finite Transition System- AFTS). AFTSen är en utökning av den klassiska Ändliga ÖvergångsSystems definitionen med ett utvecklings set som identifierar avslutande lokalaregler strategier. Eftersom AFTSen är en alternerande simulering av detutökade systemet så är en regulator som löser AFTS problemet också enlösning för det utökade systemet. Specifikationerna för problemet är givnasom Linjär Temporal Logiks formler (Linear Temporal Logic - LTL). Produktenav den icke-deterministiska AFTSen och Büchi automaten av LTLspecifikationen är definierad. En algoritm som kan hitta icke-blockerande reglerstrategier för AFTSen används för att hitta en ändlig tillståndsregulator.Den här metoden för syntetisering av regulatorer för Linjär TemporalLogiks specifikationer har använts framgångsrikt och har testats på scenariermed enstaka samt era quadrocopters i Smart Mobility Lab på KTH