Alternating RQ timed automata

Abstract

Two major difficulties in verification with timed automata are state explosion and dependence of complexity on time constants, even with restricted timing constraints. Based on the observation that a vast majority of timed automata have a very regular timing structure, We propose a class of timed automata, alternating RQ timed automata, and prove that they have simple path properties which, even with arbitrary timing constraints, yield efficient verification algorithms. In addition, the complexity of the algorithms is independent of the time constants. Next, we give graphical necessary and sufficient conditions for timed automata to be RQ alternating. Finally; we discuss verification algorithms of alternating RQ L-automata (L-processes).