Most Permissive Strategies for Games with Negation-free CTL
Authors
Ragnuson, Beinir ; Wennerstrøm, Bogi Napoleon ; Vang, Sigmundur
Term
4. term
Education
Publication year
2021
Abstract
This thesis studies controller synthesis for open systems in a branching-time setting, focusing on Game Labelled Kripke Structures (GLKS) and negation-free CTL specifications. We first encode a GLKS and formula as a labeled dependency graph using uniform rules and compute its minimum fixed point in linear time. Because branching-time synthesis is not compositional in the structure of the formula, we translate this graph into a meta-dependency graph in disjunctive normal form and identify and eliminate strategy conflicts, which lets us decide whether a winning strategy exists. To actually synthesize behavior, we introduce the fragment CTL- and provide two algorithms: one constructs the most permissive strategy (a sound and complete family containing exactly all winning strategies), and one extracts a deterministic winning strategy via alternating reachability. We show that the synthesis problem in this setting is PSPACE-hard. All algorithms are implemented and visualized in the PetriGAAL tool.
Specialet undersøger controllersyntese for åbne systemer i en forgrenet tidslogik med fokus på spilmærkede Kripke-strukturer (GLKS) og negationsfri CTL. Vi koder først en GLKS og en formel som en mærket afhængighedsgraf ud fra ensartede regler og beregner det mindste fikspunkt i lineær tid. Fordi syntese i forgrenet tid ikke er kompositionel i formulakonstruktionen, oversætter vi derefter grafen til en meta-afhængighedsgraf i disjunktiv normalform og identificerer samt udelukker strategikonflikter, hvilket gør det muligt at afgøre, om der findes en vindende strategi. For faktisk at syntetisere adfærd indfører vi fragmentet CTL- og giver to algoritmer: én, der konstruerer den mest tilladende strategi (en korrekt og fuldstændig familie, der præcis rummer alle vindende strategier), og én, der udtrækker en deterministisk vindende strategi via alternerende nåbarhed. Vi viser, at synteseproblemet i denne ramme er PSPACE-svært. Alle algoritmer er implementeret og kan visualiseres i værktøjet PetriGAAL.
[This apstract has been generated with the help of AI directly from the project full text]