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

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