Rewriting Logic Semantics and Symbolic Analysis for Parametric Timed Automata
summary
Rewriting-logic encoding of parametric timed automata yields a Maude-with-SMT symbolic reachability procedure that is proven sound and complete for PTA reachability, implements a new reachability command with folding and subsumption so exploration terminates whenever the parametric zone graph is finite, and performs parameter synthesis vs Imitator showing comparable results while allowing richer state properties (e.g., clock comparisons) and user-defined strategy-driven analyses built on real-time rewrite theories.
AI-written summary · about
chapters (7)
- 0:00Start
- 0:17Motivation
- 2:12Outline
- 9:25Rewriting Logic
- 11:36PTA to Rewrite Theories Structure
- 19:17Parameter Synthesis
- 20:38Use of the Strategy Language
related talks
24mSynthesis of Parametric Locally Symmetric Protocols from Abstract Temporal Specifications
16mParameterized Verification of Disjunctive Timed Networks
25mSymbolic Bisimulation for Open and Parameterized Systems
27mParameterized Infinite-State Reactive Synthesis
26mKater: Automating Weak Memory Model Metatheory and Consistency Checking
21mA Universal, Sound, and Complete Forward Reasoning Technique for Machine-Verifie...
15mStructural Abstraction and Refinement for Probabilistic Programs
19mSolving Infinite-State Games via Acceleration