Model checking for timed logic processes

Abstract

We apply techniques from logic programming and constraint databases to verify real time systems. We introduce timed logic processes (TLPs) as a fragment of constraint query languages over reals. We establish a formal connection between TLPs and timed automata, and between the procedure of the UPPAAL model checker for restricted temporallogic properties of timed automata and the top-down query evaluation of TLPs (with tabling in the XSB style). This connection yields an alternative implementation of the UPPAAL procedure. Furthermore, we can extend that procedure in order to accommodate more expressive properties.