Parameterized Verification of Disjunctive Timed Networks
summary
Claim: networks of timed automata with disjunctive location guards admit a single summary TA that is language-equivalent to one process in a DTN of any size. Method: compute per-guard Delta_min values by exploring zone graphs, then replace location guards with a global-time clock constraint and solve the Minreach problem with a novel zone-graph algorithm. Result: avoids exponential cutoff constructions, is implemented, and shows exponential practical speedups on clock‑synchronization case studies.
AI-written summary · about
chapters (9)
- 0:00Parameterized verification intro
- 1:52Disjunctive timed networks
- 3:56Reachability across sizes
- 5:25Existing results and approach
- 7:13Constructing the equivalent timed automaton
- 9:00Proving TA language equivalence
- 12:33Calculating Delta Min
- 14:18Experimental results
- 15:03Extensions and conclusion
related talks
29mRewriting Logic Semantics and Symbolic Analysis for Parametric Timed Automata
31mParameterized Verification of Systems with Precise (0,1)-Counter Abstraction
54mReduction theorems for effective parameterized verification of round- based distributed algorithms
42mTime-sensitive protocol: Links From Design to Implementation
24mSynthesis of Parametric Locally Symmetric Protocols from Abstract Temporal Specifications
25mProperty-agnostic base case extension for scalable verification of distributed systems
28mReasoning about Distributed Reconfigurable Systems
31mCompositional Verification of Stigmergic Collective Systems