Accelerating Synthesis of Timed Game using Async Parallelisation and GPU
Authors
Christiansen, Mathias Wienmann Biehl ; Eriksen, Oliver Vejlgaard ; Bak, Oliver Steen
Term
4. term
Education
Publication year
2024
Submitted on
2024-06-07
Abstract
This thesis investigates whether verification and controller synthesis for timed games can be accelerated by performing Difference Bound Matrix (DBM) operations massively in parallel on GPUs and by using asynchronous co‑processing. Timed (Game) Automata have infinite, uncountable state spaces that are handled symbolically via zones represented as DBMs, but this approach remains vulnerable to state‑space explosion. We extend prior work (SMAcc) with GDBM, a GPU‑based library that supports the operations needed for controller synthesis in Timed Game Automata and tackles key challenges such as non‑convex DBM subtraction during back‑propagation of winning information and dynamic GPU memory allocation. Methodologically, we develop techniques to achieve high parallelism and occupancy in CUDA, and we integrate GDBM with Uppaal and Uppaal Tiga so that the tools process the discrete state space while the continuous (DBM) computations run on the GPU in an asynchronous co‑process. Experiments show substantial gains on isolated DBM operations, including up to a 68.2× speedup for computing canonical forms versus UDBM and 10.32× versus SMAcc. These improvements translate to end‑to‑end tasks: for reachability analysis we achieve up to a 178.72× speedup over our previous work, and the asynchronous integration with Uppaal (Tiga) yields promising results. For reachability, performance is within a single order of magnitude of Uppaal, which is a major improvement over SMAcc; for controller synthesis, additional work is needed to rival Uppaal Tiga. To the best of our knowledge, this is the first use of GPUs for synthesis of timed games, and we outline directions for future enhancements.
Denne afhandling undersøger, om verifikation og controllersyntese for tidslige spillesystemer kan accelereres ved at udføre Difference Bound Matrix (DBM)‑operationer massivt parallelt på GPU og ved asynkron koprocessering. Timed (Game) Automata har en uendelig og ukontinuert tilstandsmængde, som i praksis håndteres symbolsk via zoner repræsenteret som DBM’er, men denne tilgang lider af tilstandseksplosion. Vi udvider tidligere arbejde (SMAcc) med en ny GPU‑baseret DBM‑biblioteksløsning, GDBM, der adresserer centrale udfordringer i controllersyntese for Timed Game Automata, herunder ikke‑konveks DBM‑subtraktion ved tilbagepropagering af vindende information og behovet for dynamisk hukommelsesallokering på GPU. Metodemæssigt beskriver vi teknikker til høj grad af parallelisme og occupancy i CUDA, og vi integrerer GDBM i både Uppaal og Uppaal Tiga, således at de diskrete dele håndteres i værktøjerne, mens de kontinuerte (DBM)‑operationer kører på GPU i en asynkron samarbejdsproces. Eksperimenterne viser betydelige gevinster på isolerede DBM‑operationer, herunder op til 68,2× hastighedsforøgelse for beregning af kanoniske former sammenlignet med UDBM og 10,32× i forhold til SMAcc. Disse forbedringer overføres til end‑to‑end‑opgaver: for reachability‑analyse opnås op til 178,72× forbedring i forhold til vores tidligere arbejde, og den asynkrone integration med Uppaal (Tiga) giver lovende resultater. For reachability er vi inden for en størrelsesorden af Uppaal, hvilket er en markant forbedring over SMAcc; for controllersyntese kræves yderligere arbejde for at matche Uppaal Tiga. Afhandlingen peger på fremtidige forbedringsmuligheder og præsenterer, efter vores bedste viden, den første GPU‑baserede tilgang til syntese af timed games.
[This apstract has been generated with the help of AI directly from the project full text]