AbstractsEngineering

Automatic Control Design Synthesis under Metric Interval Temporal Logic Specifications

by Sofie Andersson




Institution: KTH Royal Institute of Technology
Department:
Year: 2016
Keywords: Engineering and Technology; Electrical Engineering, Electronic Engineering, Information Engineering; Teknik och teknologier; Elektroteknik och elektronik
Posted: 02/05/2017
Record ID: 2101509
Full text PDF: http://urn.kb.se/resolve?urn=urn:nbn:se:kth:diva-187716


Abstract

The problem of synthesizing controllers for motion planning of multi-agent systems under Linear Temporal Logic (LTL) high-level specifications has been of great interest and has been widely studied over the last years. However, LTL cannot handle time constraints as specifications. The time aspect would allow more complicated and specific tasks and it is therefore desirable to incorporate. This work aims to determine how control synthesis for a continuous linear system can be performed based on Metric Interval Temporal Logic (MITL), which is able to handle desired time constraints to high-level specifications. Firstly, a control design synthesis method for a single-agent, based on previous work within both the field of LTL and MITL is presented. Secondly, a control design synthesis method for multi-agent systems considering both local an global MITL specifications is presented. Extended simulations has been performed in MATLAB environment demonstrating the two proposed methodologies. The result shows that the methods guarantee that the MITL specifications are satisfied, for all cases for which a solution is found. ; Problemet gällande regulator syntetisering for rörelse planering av fler-agents system under Line-ar Temporal Logic (Linjär Temporal Logik=LTL) hög-nivå specifikationer har varit av stort intresse och har studerats brett under de senaste åren. LTL kan emellertid inte hantera tidsbegränsningar som specifikationer. Tidsaspekten skulle tillåta mer komplicerade och specifika uppgifter. Det är därför önskvärt att inkorporera. Målet med det här arbetet är att fastställa hur regulator syntetisering för ett kontinuerligt, linjärt system kan utföras utgående från Metric Interval Temporal Logic (Metrisk Intervall Temporal Logic =MITL), en gren av Temporal Logik som kan hantera de önskvärda tidsbegränsningarna för högnivå specifikationer. Först presenteras en metod för att syntetisera regulatorer för en-agents system. Metoden är baserad på tidigare arbeten inom fälten LTL och MITL. Sedan presenteras en metod för att syntetisera regulatorer för fler-agents system som ¨önskas uppfylla såväl lokala som globala MITL specifikationer. Utbredda simulationer har genomförts i MATLAB miljö för att demonstrera de två˚ föreslagna metoderna. Resultatet visar att metoderna garanterar att MITL specifikationerna är uppfyllda för alla fall för vilka en lösning hittas.