From games to executables!
Authors
Holleufer, Kenneth Blanner ; Rosenkilde, Jesper Brix
Term
4. term
Education
Publication year
2009
Abstract
This thesis investigates how game-based control strategies synthesized by UPPAAL TIGA can be turned into executable controllers for real systems. We first introduce control-theoretic modeling from input–output models through hybrid and discrete-event systems, and present timed automata with symbolic techniques (regions and zones). Framing control as real-time games between a controller and the environment, we discuss strategy synthesis in UPPAAL TIGA, address pitfalls such as Zeno runs via model adaptations, and propose pruning to remove unreachable parts of synthesized strategies. As a case study, we model a LEGO brick sorter (conveyor belt, color sensor, piston) under varying assumptions: full and partial observability, symmetry reduction, cycle elimination (acyclic), sequentialization, and a fully discrete variant. We compare these models with respect to state-space size, strategy size, and generation time. Finally, we implement an end-to-end toolchain that encodes TIGA strategies compactly using clock difference diagrams combined with binary decision diagrams, provides a Java runtime for strategy evaluation on a LEGO NXT controller, and includes a parser/code generator that translates TIGA output into executable code. Overall, the work demonstrates that strategies from timed-automata models can be automatically deployed to control the sorter and reconfigured by changing the model or property without manual reprogramming.
Denne afhandling undersøger, hvordan spilbaserede kontrolstrategier syntetiseret med UPPAAL TIGA kan omsættes til eksekverbare controllere for fysiske systemer. Vi introducerer først kontrolteori fra input–output-modellering over hybride systemer til diskrete hændelsessystemer og gennemgår tidsautomater med symbolske teknikker (regioner og zoner). Med udgangspunkt i realtidsspil mellem controller og omgivelser drøfter vi strategisyntese i UPPAAL TIGA, håndterer faldgruber som Zeno-løb via modeltilpasninger og foreslår beskæring af strategier for at fjerne utilgængelige dele. Som casestudie modellerer vi en LEGO-klodsesorterer (transportbånd, farvesensor, stempel) under forskellige antagelser: fuld og delvis observabilitet, symmetrireduktion, cykelfjernelse (acyklisk), sekventialisering samt en fuldt diskret variant. Disse modeller sammenlignes mht. tilstandsrumsstørrelse, strategistørrelse og genereringstid. Til slut implementerer vi en ende-til-ende værktøjskæde, der kompakt koder TIGA-strategier med klokdifferensdiagrammer kombineret med binære beslutningsdiagrammer, leverer en Java-runtime til evaluering på en LEGO NXT-controller og inkluderer en parser/kodegenerator, som oversætter TIGA-uddata til eksekverbar kode. Samlet demonstrerer arbejdet, at strategier fra tidsautomatsmodeller kan implementeres automatisk til at styre sorteringssystemet og nemt omkonfigureres ved at ændre model eller egenskab uden manuel genprogrammering.
[This apstract has been generated with the help of AI directly from the project full text]