Convergence proofs for Simulated Annealing falsification of safety properties

The problem of falsifying temporal logic properties of hybrid automata can be posed as a minimization problem by utilizing quantitative semantics for temporal logics. Previous work has used a variation of Simulated Annealing (SA) to solve the problem. While SA is known to converge to the global minimum of a continuous objective function over a closed and bounded search space, or when the search space is discrete, there do not exist convergence proofs for the cases addressed in that previous work. Namely, when the objective function is discontinuous, and when the objective is a vector-valued function. In this paper, we derive conditions and we prove convergence of SA to a global minimum in both scenarios. We also consider matters affecting the practical performance of SA.