Parametric timed automata (PTA) extends timed automata (TA) with parameters instead of fixed timing constraints, which provides the flexibility to accommodate uncertainties during the design phase. Once the parametric model is obtained, parameter synthesis methods are applied to find the optimal parameter values such that the resulting timed automaton satisfies the specifications.
In this thesis, parameter synthesis strategies for parametric timed automata are developed. The proposed approaches involve accumulating parameter constraints while exploring the automata graph in a depth-first manner. Realizability problems of encountered paths during the graph search are encoded as Mixed Integer Linear Programming (MILP) or Non-Linear Programming (NLP) problems; then, those problems are evaluated in different ways depending on the given specifications. For specifications where a single witness is enough, e.g., reachability, the depth-first search returns the first parameter constraint that makes a path ending in an accepting state realizable. For specifications where no witness must exist, e.g., safety, parameter constraints are found by applying quantifier elimination on encoded problems and accumulated along the depth-first traversal. Depth-first traversal is optimized via prunning unrealizable branches and is guaranteed to terminate via the proposed novel cycle analysis methods. The collected constraints through the depth-first search guarantee that a parameter valuation satisfying these constraints solves the synthesis problem. The developed algorithms are extended to generate the optimal parameter values for a given criteria. The correctness and completeness of the proposed algorithms are presented. All the results are depicted via examples.