From games to executables!: Implementaions of strategies from UPPAAL TIGA
Author
Rosenkilde, Jesper
Term
2. term
Education
Publication year
2009
Pages
105
Abstract
Denne afhandling undersøger, hvordan strategier syntetiseret af modeltjekker-værktøjet UPPAAL TIGA kan omdannes fra spilteoretiske planer til eksekverbare controllere for fysiske systemer. Den giver først en tilgængelig introduktion til reguleringsteori, timed automata og symbolske teknikker (regionsgrafer og zoner), der gør uendelige tilstandsrumsmodeller håndterbare. Dernæst formuleres realtids-spil mellem controller og miljø, strategisyntese i UPPAAL TIGA forklares, og praktiske udfordringer som Zeno-forløb og beskæring af utilgængelige dele af syntetiserede strategier adresseres. Som case anvendes en LEGO-baseret klodessorterer, hvor forskellige modelleringsvarianter (fra fuld information til partiel observabilitet, symmetrireduktion, sekventielle og acykliske strukturer samt en diskret abstraktion) sammenlignes med hensyn til tilstandsrummets størrelse, genereringstid og strategistørrelse. For at afvikle strategierne foreslås en kompakt hybridrepræsentation, der kombinerer klokkedifferensdiagrammer med binære beslutningsdiagrammer, implementeret som et Java-runtime på en LEGO NXT-controller, samt en parser/kodegenerator, der omsætter UPPAAL TIGA-output til kode på enheden. Samlet demonstrerer arbejdet, at strategier fra UPPAAL TIGA kan deployeres automatisk til at styre klodessorteren, og eksperimenterne belyser, hvordan modelleringsvalg påvirker strategigenerering; detaljerede kvantitative resultater fremgår ikke af dette uddrag.
This thesis investigates how strategies synthesized by the UPPAAL TIGA model checker can be transformed from game-theoretic plans into executable controllers for real systems. It first provides an accessible introduction to control theory, timed automata, and symbolic techniques (region graphs and zones) that make infinite state-space models tractable. It then formulates controller–environment real-time games, explains strategy synthesis in UPPAAL TIGA, and addresses practical issues such as Zeno runs and pruning unreachable parts of synthesized strategies. Using a LEGO-based brick sorter as a case study, the work explores multiple modeling variants (from full information to partial observability, symmetry reduction, sequential and acyclic structures, and a discrete abstraction) and compares their impact on state-space size, generation time, and strategy size. To execute strategies, it proposes a compact hybrid representation combining clock difference diagrams with binary decision diagrams, implements a Java runtime on a LEGO NXT controller, and builds a parser/code generator that converts UPPAAL TIGA output into device code. Overall, the pipeline demonstrates that strategies produced in UPPAAL TIGA can be automatically deployed to control the brick sorter, with experiments highlighting how modeling choices affect strategy generation; detailed quantitative results are not provided in this excerpt.
[This summary has been generated with the help of AI directly from the project (PDF)]
Documents