Decidable verification for reducible timed automata specified in a first order logic with time

• Published in: Theoretical computer science 2002-03, Vol.275 (1), p.347-388
• Main Authors: Beauquier, Danièle, Slissenko, Anatol
• Format: Article
• Language: English
• Subjects: Algebra; Applied sciences; Automata. Abstract machines. Turing machines; Category theory, homological algebra; Computer science; control theory; systems; Decidable class; Exact sciences and technology; First order logic; Logic and foundations; Mathematical logic, foundations, set theory; Mathematics; Recursion theory; Sciences and techniques of general use; Theoretical computing; Timed automata; Verification
• ISSN: 0304-3975; 1879-2294
• DOI: 10.1016/S0304-3975(01)00186-4

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 language close to the natural one, 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, “finite refutability” and “finite satisfiability”, are undecidable in the general case. However, “finite refutability” is often easy to verify. On the other hand, we give a sufficient condition, namely reducibility, which ensures the “finite satisfiability” for timed automata, and we prove that the reducibility is decidable. This is the main result of the paper. As a consequence the verification of any finitely refutable requirements is decidable for reducible timed automata.