Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Multi agent control with LTL specifications and abstraction with input memories
KTH, School of Electrical Engineering (EES), Automatic Control.
2017 (English)Independent thesis Advanced level (degree of Master (Two Years)), 20 credits / 30 HE creditsStudent thesis
Abstract [en]

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.

Abstract [sv]

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.

Place, publisher, year, edition, pages
2017. , p. 74
Series
TRITA-EE, ISSN 1653-5146 ; 2017:014
National Category
Electrical Engineering, Electronic Engineering, Information Engineering
Identifiers
URN: urn:nbn:se:kth:diva-203510OAI: oai:DiVA.org:kth-203510DiVA, id: diva2:1082130
Educational program
Master of Science in Engineering - Electrical Engineering
Available from: 2017-03-15 Created: 2017-03-15 Last updated: 2017-03-15Bibliographically approved

Open Access in DiVA

fulltext(1838 kB)50 downloads
File information
File name FULLTEXT01.pdfFile size 1838 kBChecksum SHA-512
354d593ed5049c0bef794cbe134b10771fa8e8f37a72297fe257c4ecd53a52dd93a0ba2cca948c98821c8c651e89b26a7fef7f635bbdc4ff71e0a7280a956703
Type fulltextMimetype application/pdf

By organisation
Automatic Control
Electrical Engineering, Electronic Engineering, Information Engineering

Search outside of DiVA

GoogleGoogle Scholar
Total: 50 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

urn-nbn

Altmetric score

urn-nbn
Total: 126 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf