Symbolic Encodings of Timed Games with Incomplete Information
Daniel Dahrendorf
In this thesis we provide two symbolic encodings for timed games with incomplete information. We take two models 11,8 and transform them into symbolic game structures which can be used as input for the counterexample-guided abstraction refinement approach for timed games with incomplete information from 14. We restrict the specifications of the models to be deterministic, fix the resources of the controller and focus on safety games. The challenge is to encode the two models, which are based on timed (game) automata and using different definitions of timed games and specifications. The results are symbolic game structures defined by variables, by their domain and by formulas over predicates. The correctness of the encodings is proved. Since 14 provides sufficient conditions for termination of the refinement loop we give an alternative proof for the decidability of the controller synthesis problem for the considered class of timed games. Further, we provide and implementation for the encoding of the model from 11.
Master Thesis.