Efficient Convex Zone Merging in Parametric Timed Automata
arXiv:2212.04802 · doi:10.1007/978-3-031-15839-1_12
Abstract
Parametric timed automata are a powerful formalism for reasoning on concurrent real-time systems with unknown or uncertain timing constants. Reducing their state space is a significant way to reduce the inherently large analysis times. We present here different merging reduction techniques based on convex union of constraints (parametric zones), allowing to decrease the number of states while preserving the correctness of verification and synthesis results. We perform extensive experiments, and identify the best heuristics in practice, bringing a significant decrease in the computation time on a benchmarks library.
arXiv commentThis is the author version of the manuscript of the same name published in the proceedings of the 20th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2022)
References in corpus (6)
- What's decidable about parametric timed automata?
- Better abstractions for timed automata
- Efficient Emptiness Check for Timed Büchi Automata (Extended version)
- A Benchmarks Library for Extended Parametric Timed Automata
- Divide and Conquer: Variable Set Separation in Hybrid Systems Reachability Analysis
- Language Preservation Problems in Parametric Timed Automata