Efficiently Finding Ratio-Optimal Infinite Cycles in Doubly-Priced Timed Automata
Authors
Johansen, Nicklas Slorup ; Knorborg, Kristian Ødum ; Tollund, Rasmus Grønkjær
Term
4. term
Education
Publication year
2023
Submitted on
2023-06-08
Pages
71
Abstract
This thesis studies how to efficiently find ratio-optimal infinite cycles in doubly priced (cost–reward) timed automata, a problem that arises in optimizing recurring processes in real-time systems and is known to be PSPACE-complete. The main contribution is the symbolic λ-deduction algorithm, which reduces the task to a single priced automaton and uses priced zones to iteratively improve the best cycle found. We prove its correctness and termination, and further show that the effect of traversing a path or cycle on a symbolic state’s cost function can be captured as an affine transformation, enabling efficient detection of negative symbolic cycles. We also propose a symbolic approach based on binary decision diagrams (BDDs) that encodes the transition relation and seeks the optimal cycle via transitive closure; despite theoretical value, this approach performs poorly in practice. In experiments on practical models, we compare against a concrete corner-point abstraction baseline (CP-MCR using Howard’s algorithm) and find that symbolic λ-deduction outperforms the concrete method in some cases and remains unaffected by large clock constants, whereas the concrete approach suffers exponential slowdown.
Denne afhandling undersøger, hvordan man effektivt finder forholdsoptimale uendelige cykler i dobbeltprismærkede (cost–reward) tidsautomater, et problem med praktisk relevans for optimering af processer i realtidssystemer og kendt for sin høje kompleksitet. Vores hovedbidrag er algoritmen symbolic λ-deduction, der reducerer problemet til en enkelt prismærket automat og anvender prismærkede zoner til trinvist at forbedre den hidtil bedste cyklus. Vi beviser algoritmens korrekthed og terminatede egenskaber, og viser desuden, at ændringen i en symbolsk tilstands prisfunktion efter en sti eller cyklus kan udtrykkes som en affin afbildning, hvilket gør det muligt effektivt at identificere negative symbolske cykler. Derudover præsenterer vi en symbolsk metode baseret på binære beslutningsdiagrammer (BDD’er), der indkoder overgangsrelationen og søger den optimale cyklus via transitiv lukning; metoden har dog meget dårlig praktisk ydeevne, om end teoretisk interesse. I en eksperimentel evaluering sammenligner vi vores forslag med en konkret hjørnepunktsabstraktionsbaseret reference (CP-MCR med Howard’s algoritme) og viser, at symbolic λ-deduction i nogle tilfælde overgår den konkrete tilgang og forbliver upåvirket af store urkonstanter, mens den konkrete metode udviser eksponentiel afmatning.
[This apstract has been generated with the help of AI directly from the project full text]
Keywords