Artifact for TACAS 2019 paper: Minimal-Time Synthesis for Parametric Timed Automata

This artifact contains the means to reproduce the experimental results from the<br>paper. In the paper we propose algorithms that synthesize a/all parameter<br>valuation(s) in a PTA, such that the time to reach the target location is<br>minimized. Additionally, we also propose algorithms that synthesize a/all<br>parameter valuation(s) that minimize a specific parameter.<br><br>We consider the following algorithms in our experiments:<br>- Synth: the classical synthesis algorithm (without time minimization)<br>- MTSynth: our minimal-time synthesis algorithm<br>- MPSynth: our minimal-parameter synthesis algorithm (which is used to compute<br> the minimal time)<br>- MTSynth-noRed: Our MTSynth algorithm without using state-space reductions<br>- MTReach: our minimal-time reachability algorithm (that returns at least one<br> parameter valuation that reaches the target location in minimal time)<br>- MPReach: our minimal-parameter reachability algorithm (see MTReach)<br><br>For the experiments, we collected 68 PTA models and properties from the<br>IMITATOR benchmarks library, and ran each experiment (algorithm+model<br>combination).<br><br>The most interesting result is that the minimal-time synthesis version is in<br>general faster in computing results when compared to the classical synthesis<br>algorithm. We can also observe that MTSynth is faster than MPSynth (in MTSynth<br>we use a shortest-path search, and in MPSynth we do not). When comparing<br>reachability with synthesis, we see that the results are fairly similar, with<br>only a few instances in which only reachability is computable in the allowed<br>time.<br><br><br>