Decidable Verification for Reducible Timed Automata

We consider one type of first order timed logic (FOTL) with explicit continuous time. FOTL is sufficiently expressible from the user’s point of view to rewrite directly requirements specifications often given in a natural language, and it permits to represent the set of runs of timed programs. Thus, FOTL is apt to formalize the verification problem for timed systems. Our main goal is to describe in semantical terms interesting decidable classes of the verification problem within this setting. We prove that under some finiteness properties of the requirements and algorithm specifications the verification problem represented in FOTL becomes decidable. The finiteness properties we introduce, “local refutability” and “finite satisfiability”, are undecidable in the general case. However, “local refutability” is often easy to verify. On the other hand, we give a sufficient condition, namely reducibility, which assures the “finite satisfiability” for timed automata, and we prove that the reducibility is decidable. As a consequence all the locally refutable properties (e.~g. “the average value of clocks is always bounded by a given constant”) are proven to be decidable for reducible timed automata.