Talk "Symbolic Analysis and Parameter Synthesis for Parametric Timed Automata and Petri Nets using Maude with SMT Solving"

by Peter Ölveczky

Tue, 06 February 2024 at 03:30 pm in Salzburg, Austria

Joint work with: Carlos Olarte (U Sorbonne Paris-Nord), Laure Petrucci (U Sorbonne Paris-Nord), Kyngmin Bae (POSTECH), Jaime Arias (U Sorbonne Paris-Nord), Fredrik Rømming (Cambridge)

Abstract: We use the rewriting logic framework Maude--which has been equipped with support for SMT solving--to provide semantics, symbolic reachability and other kinds of analyses, and synthesis of unknown system parameters for both networks of parametric timed automata with global variables (NPTAVs) and parametric interval time Petri nets with inhibitor arcs (PITPNs). We develop symbolic reachability analysis methods in Maude-with-SMT which are sound and complete for the corresponding models (NPTAVs and PITPNs). Furthermore, our Maude-with-SMT reachability analyses terminate when the reachable symbolic state space of the NPTAV, respectively, the PITPN, is finite. We can then perform most of the analysis and parameter synthesis methods provided by the specialized state-of-the-art tools Imitator and Romeo for the respective domains. We also benchmark our methods, and show that in a number of cases they outperform Romeo. The practical contributions are: (i) providing new analysis methods, and sometimes better performance, for NPTAVs and TIPNSs; and (ii) studying and developing symbolic analysis methods for interesting classes of real-time systems as steps in our quest to provide symbolic analysis for more general real-time systems in the Real-Time Maude tool.