Symbolic analysis and parameter synthesis for networks of parametric timed automata with global variables using Maude and SMT solving

This paper presents a rewriting logic "interpreter" for networks of parametric timed automata with global variables (NPTAVs) in Real-Time Maude style. Since explicit-state analysis is not sound and complete for such dense-time systems, we explain how our real-time rewrite theory can be systematically transformed into a rewrite theory that is amenable to symbolic analysis using the integration of Maude with SMT solving. We show that symbolic reachability analysis using Maude-with-SMT of the resulting rewrite theory is sound and complete for the NPTAV reachability problem. We extend and optimize standard Maude-with-SMT reachability analysis with folding and merging of symbolic states, so that the analysis terminates when the symbolic state space of the NPTAV is finite. These procedures rely on a subsumption relation that requires eliminating existentially quantified SMT variables. We have therefore implemented the Fourier-Motzkin quantifier elimination algorithm, thereby making our rewrite theory executable with any SMT solver connected to Maude. We show how we can provide most reachability and parameter synthesis analysis methods provided by Imitator, a state-of-the-art tool for NPTAVs. We compare the performance of our analysis methods with those of Imitator on a wide range of benchmarks, with the expected outcome. The practical contributions are two-fold: providing new analysis methods for NPTAVs-e.g., allowing more general state properties and supporting reachability analysis combined with user-defined execution strategies-not supported by Imitator, and developing symbolic analysis methods for both real-time rewrite theories and rewrite theories in general.