Costs and rewards in priced timed automata

Abstract We consider Pareto analysis of multi-priced timed automata (MPTA) having multiple observers recording costs (to be minimised) and rewards (to be maximised) along a computation. We study the Pareto Domination Problem, which asks whether it is possible to reach a target location such that the accumulated costs and rewards Pareto dominate a given vector. We show that this problem is undecidable in general, but decidable for MPTA with at most three observers. We show the problem to be PSPACE-complete for MPTA recording only costs or only rewards. We also consider an approximate Pareto Domination that is decidable in exponential time with no restrictions on types and number of observers. We develop connections between MPTA and Diophantine equations. Undecidability of the Pareto Domination Problem is shown by reduction from Hilbert's 10th Problem, while decidability for three observers entails translation to a decidable fragment of arithmetic involving quadratic forms.