A CLP Proof Method for Timed Automata
Joxan Jaffar, Andrew Santosa and Razvan Voicu
Abstract
Constraint Logic Programming (CLP) has been used to model programs and
transition systems for the purpose of verification problems. In
particular, it has been used to model Timed Safety Automata (TSA). In
this paper, we start with a systematic translation of TSA into CLP.
The main contribution is an expressive assertion language and a new
CLP inference method for proving assertions. A distinction of the
assertion language is that it can specify important properties beyond
traditional safety properties. We highlight one important property:
that a system of processes is \underline{\em symmetric}. The new
inference mechanism is based upon the well-known method of tabling in
logic programming. It is distinguished by its ability to use assertions
that are not yet proven, using a principle of {\it coinduction}. Apart
from given assertions, the proof mechanism can also prove implicit
assertions such as discovering a lower or upper bound of a variable.
Finally, we demonstrate significant improvements over state-of-the-art
systems using standard TSA benchmark examples.