nptav2maude
We give a rewriting logic semantics for parametric timed automata with global variables (PTAVs) and show that symbolic reachability analysis using Maude-with-SMT is sound and complete for the PTA reachability problem. We refine standard Maude-with-SMT reachability so that the analysis terminates when the symbolic state space of the PTA is finite. Besides reachability, the rewrite theory can be also used for parameter synthesis. This repository includes benchmarks comparing our methods and Imitator.
Getting started
The project was tested in Maude 3.2 and Maude SE. A script written in Python 3.10 is used to parse Imitator input files into Maude files.
Maude files
The specification can be found in the folder maude
. It includes the following files:
- TODO
See the headers of each file for further information.
Parser
The parser of Imitator models into Maude theories can be found in nptav2maude
.
See the file README for further information about its
implementation in Python.
Benchmarks
See the file README for further information about the benchmarks comparing the performance of Imitator and our analyses.