ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Thu 11 Apr 2019 11:30 - 12:00 at SUN I - Synthesis Chair(s): Roland Meyer

Parametric timed automata (PTA) extend timed automata by allowing parameters in clock constraints. Such a formalism is for instance useful when reasoning about unknown delays in a timed system. Using existing techniques, a user can synthesize the parameter constraints that allow the system to reach a specified goal location, regardless of how much time has passed for the internal clocks. We focus on synthesizing parameters such that not only the goal location is reached, but we also address the following questions: what is the minimal time to reach the goal location? and for which parameter values can we achieve this? We analyse the problem and present an algorithm that solves it. We also discuss and provide solutions for minimizing a specific parameter value to still reach the goal. We empirically study the performance of these algorithms on a benchmark set for PTAs and show that minimal-time synthesis is more efficient to compute than the standard synthesis algorithm for reachability.

Thu 11 Apr

tacas-2019-papers
10:30 - 12:30: TACAS 2019 - Synthesis at SUN I
Chair(s): Roland MeyerTechnical University of Braunschweig
tacas-2019-papers10:30 - 11:00
Talk
Link to publication
tacas-2019-papers11:00 - 11:30
Talk
Nathalie CauchiUniversity of Oxford, Alessandro AbateUniversity of Oxford
Link to publication
tacas-2019-papers11:30 - 12:00
Talk
Étienne AndréLIPN, CNRS UMR 7030, Université Paris 13, Vincent BloemenUniversity of Twente, Laure PetrucciUniversité Paris 13, Jaco van de PolAarhus University
Link to publication
tacas-2019-papers12:00 - 12:30
Talk
Link to publication