Efficient Convex Zone Merging in Parametric Timed Automata

TL;DR

This paper introduces convex zone merging techniques for parametric timed automata to efficiently reduce state space and improve analysis times while maintaining correctness.

Contribution

It proposes new merging reduction methods based on convex unions of constraints, with heuristics validated through extensive experiments.

Findings

Significant decrease in computation time on benchmark library

Effective heuristics for convex zone merging identified

Reduction in state space without losing verification accuracy

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.