UPPAAL CORA

UPPAAL CORA is a branch of UPPAAL for Cost Optimal Reachability Anslysis developed by the UPPAAL team as part of the VHS and AMETIST projects. Whereas UPPAAL uses timed automata as its modelling language, UPPAAL CORA uses linearly priced timed automata (LPTA). Given an LPTA model, UPPAAL CORA finds the optimal paths to a state satisfying some goal conditions. Optimal here means the path with the lowest accumulated cost. UPPAAL CORA provides a number of extensions to the modelling language of UPPAAL, that allows the user to convey additional insight about the model to the tool, which in turn can improve the performance of UPPAAL CORA. In particular, it is possible to annotate the model with an estimate of the remaining cost for reaching a state satisfying the goal conditions. This can significantly reduce the time required for finding a good or an optimal solution.