Parameter synthesis for timed automata via path analysis

Date

2023-9-07

Author

Sucu, Burkay

Metadata

Show full item record

This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.

Item Usage Stats

73
views

52
downloads

Cite This

Parametric timed automata (PTA) extends timed automata (TA) with parameters instead of fixed timing constraints, providing 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 pruning unrealizable branches and 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.

Subject Keywords

Parametric timed automata, Parameter synthesis, Safety, Existential liveness, Existential reachability, MILP, NLP

URI

https://hdl.handle.net/11511/105547

Collections

Graduate School of Natural and Applied Sciences, Thesis