@inproceedings{da3b00ccd092437a86f08325d040c523,
title = "Minimal-time synthesis for parametric timed automata",
abstract = "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 a semi-algorithm to solve 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 reachability synthesis is more efficient to compute than the standard synthesis algorithm for reachability. Data or code related to this paper is available at: [26].",
author = "{\'E}tienne Andr{\'e} and Vincent Bloemen and Laure Petrucci and \{van de Pol\}, Jaco",
year = "2019",
month = jan,
day = "1",
doi = "10.1007/978-3-030-17465-1\_12",
language = "English",
isbn = "978-3-030-17465-1",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "211--228",
editor = "Lijun Zhang and Tom{\'a}{\v s} Vojnar",
booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",
address = "Germany",
note = "25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019 , TACAS 2019 ; Conference date: 06-04-2019 Through 11-04-2019",
}