Tabled resolution and constraints for model checking real-time systems and infinite-state systems

We present a computational framework based on tabled resolution and constraint processing for verifying real-time systems. We also discuss the implementation of this framework in the context of the XMC/RT verification tool. For systems specified using timed automata, XMC/RT offers backward and forward reachability analysis, as well as timed modal mu-calculus model checking. It can also handle timed infinite-state systems, such as those with unbounded message buffers, provided the set of reachable states is finite. We illustrate this capability on a real-time version of the leader election protocol. XMC/RT can also function as a model checker for untimed systems. Despite this versatility, preliminary benchmarking experiments indicate that XMC/RT's performance remains competitive with that of other real-time verification tools. The model-checking algorithm used in XMC/RT is based on the Alur and Dill region-graph construction for timed automata. We further show that region-graph-based techniques can be applied to much more general kinds of systems, including asynchronous untimed systems over unbounded integer variables. We follow this approach in proving that the model-checking problem for the n-process Bakery algorithm is decidable, for any fixed n. We also show that region-graph-based techniques are applicable to Rational Relational Automata.