Controller Synthesis by Solving Multi Weighted Games
Authors
Nielsen, Søren Moss ; Jensen, Lasse Steen ; Kaufmann, Isabella
Term
3. term
Education
Publication year
2016
Submitted on
2016-12-20
Pages
62
Abstract
Dette speciale undersøger controllersyntese gennem spilteori: at bygge en controller bliver til opgaven at beregne en vindende strategi mod et miljø, der kan modarbejde den. Vi fokuserer på vægtede spil, hvor hvert træk har en eller flere numeriske vægte (for eksempel omkostninger eller gevinster), og vi ser på flere typer strategier. Vi rangerer disse strategityper i et hierarki efter deres udtrykskraft, det vil sige hvor meget adfærd de kan beskrive. Vi introducerer en vægtet computation tree logic, et formelt sprog til at udtrykke kvantitative egenskaber ved sådanne spil. Vi viser, at det generelt er uafgørligt at afgøre, om en specifikation i denne logik kan opfyldes. Til gengæld identificerer vi et afgørligt del-sprog, begrænset til nåbarhed med øvre grænser, og vi giver også kompleksitetsresultater for synteseproblemet inden for dette del-sprog. Endelig præsenterer vi to metoder til at syntetisere strategier i 1-vægtede spil: (1) vi udvider attraktormængde-metoden med vægte, hvilket giver en global algoritme med polynomiel tidskompleksitet, og (2) vi viser, hvordan en strategi kan udtrækkes ved hjælp af en præ-fikspunkt-tilordning på en symbolsk afhængighedsgraf.
This thesis studies controller synthesis through the lens of game theory: building a controller becomes the task of computing a winning strategy against an environment that may act adversarially. We focus on weighted games, where each move carries one or more numerical weights (for example, costs or rewards), and we examine several kinds of strategies. We arrange these strategy types in a hierarchy by expressiveness, meaning how much behavior they can capture. We introduce a weighted computation tree logic, a formal language for expressing quantitative properties of such games. We prove that, in general, deciding whether a specification in this logic can be satisfied is undecidable. In contrast, we identify a decidable sub-logic restricted to reachability with upper bounds, and we provide complexity results for the synthesis problem under this fragment. Finally, we present two methods to synthesize strategies in 1-weighted games: (1) we extend the attractor-set method with weights, yielding a global algorithm with polynomial-time complexity, and (2) we show how to extract a strategy using a pre-fixed-point assignment on a symbolic dependency graph.
[This abstract was generated with the help of AI]
Keywords
Documents
Other projects by the authors
Nielsen, Søren Moss:
Jensen, Lasse Steen:
Kaufmann, Isabella: