pta2maude

We give a rewriting logic semantics for parametric timed automata (PTAs) 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.

Details about the translation can be found in this paper.

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 includes the following files:

• pta-base: Sorts for defining locations, states and constrained terms.
• meta-pta: Reachability procedures with folding.
• coffee.maude: Example of the coffee machine using the command smt-search.
• coffee-folding: Example of the coffee machine using folding.
• coffee-strategy: Example using the strategy language to constraint the behavior of the PTA.
• ex-fig3a, ex-fig3b, ex-fig3b-folding: Examples in Figure 3 in the paper.

See the headers of each file for further information.

Parser

See the file README for further information about the parser implemented in Python, translating Imitator files into Maude theories.

Benchmarks

See the file README for further information about the benchmarks comparing the performance of Imitator and our analyses.