Control Synthesis for Parametric Timed Automata under Unavoidability Specifications

Timed automata (TA) is used for modeling systems with timing aspects. A TA extends a finite automaton with a set of real valued variables called clocks, that measure the time and constraints over the clocks guard the transitions. A parametric TA (PTA) is a TA extension that allows parameters in clock constraints. In this paper, we focus on synthesis of a control strategy and parameter valuation for a PTA such that each run of the resulting TA reaches a target location within the given amount of time while avoiding unsafe locations. We propose an algorithm based on depth first analysis combined with an iterative feasibility check. The algorithm iteratively constructs a symbolic representation of the possible solutions, and employs a feasibility check to terminate the exploration along infeasible directions. Once the construction is completed, a mixed integer linear program is solved for each candidate strategy to generate a parameter valuation and a control strategy pair. We present a robotic planning example to motivate the problem and to illustrate the results.