-
Notifications
You must be signed in to change notification settings - Fork 0
/
hej
1 lines (1 loc) · 1.06 KB
/
hej
1
We investigate the \textit{Synthesis Problem} in a time-branching setting and show that it is PSPACE-hard. We encode a \gls{glts} together with a \gls{ctl} formula as a labeled dependency graph, then calculate the minimum fixed-point. This method has been shown to be successful in deciding problems like equivalence checking and model checking. Since synthesis in a time-branching setting is not compositional in the structure of the formula, this method alone is not enough. We solve the \textit{Synthesis Problem} by translating the resulting labeled dependency graph into a a Meta dependency graph, which is in disjunctive normal form. To find a strategy we first construct the most permissive strategy, which is a sound and complete family of strategies (all strategies in the family are winning strategies and all winning strategies are in the family). Next we present an algorithm for extracting a strategy from the most permissive instance. Finally we implement all algorithms in the tool PetriGAAL, along with support for visualizing all graphical structures contained herein.