Model checking logic WCTL with multi constrained modalities on one clock priced timed automata

We consider the model of priced timed automata, an extension of timed automata and study the model checking problem of logic WCTL with multi constrained modalities. For simple modalities, it is known that this is decidable [10] for one clock priced timed automata, and is not [14] when the number of clocks is more than one. For the model of priced timed automata with 2 stopwatch costs having no discrete costs, we give an algorithm for model checking the existential fragment of WCTL with multi constrained modalities. The algorithm runs in time that is doubly exponential in the size of the input(automaton, formula)