Delayed Constraints in Narrowing for the Logic-Based Analyses of Real-Time Systems
The formal analysis of real-time systems must address two dimensions of infiniteness: an unbounded number of agents and messages, and a potentially infinite state space induced by dense time. We present a novel narrowing-based verification method that deals with both dimensions. Our approach integrates (i) rewriting modulo SMT for symbolic representation of timing constraints, (ii) narrowing with logical variables to reason about systems with an unknown number of agents, and (iii) a constraint store over partially instantiated terms, in the style of constraint logic programming. We further introduce a folding mechanism that, under certain conditions, ensures termination of the symbolic analysis. The method has been implemented as an extension of the Maude rewriting engine. We evaluate the approach by verifying the correctness of a timed mutual exclusion protocol without imposing bounds on the number of participating processes. Moreover, we show that the framework uniformly supports the analysis of other real-time models, including parametric timed automata with unspecified components that our method can synthesize. Our results suggest that the proposed framework provides a sound and expressive basis for the symbolic verification of real-time rewrite theories.