Zone extrapolations in parametric timed automata

TL;DR

This paper explores extending zone extrapolation techniques to parametric timed automata (PTAs), proposing new definitions based on M-extrapolation, which improve analysis efficiency and enable solving previously unsolvable benchmarks.

Contribution

It introduces novel extrapolation definitions for PTAs and demonstrates their effectiveness in reducing computation time and enabling termination of complex benchmarks.

Findings

Decreased computation time in PTA analysis

Enabled termination of previously unsolvable benchmarks

Proposed correct and practical extrapolation methods for PTAs

Abstract

Timed automata (TAs) are an efficient formalism to model and verify systems with hard timing constraints, and concurrency. While TAs assume exact timing constants with infinite precision, parametric TAs (PTAs) leverage this limitation and increase their expressiveness, at the cost of undecidability. A practical explanation for the efficiency of TAs is zone extrapolation, where clock valuations beyond a given constant are considered equivalent. This concept cannot be easily extended to PTAs, due to the fact that parameters can be unbounded. In this work, we propose several definitions of extrapolation for PTAs based on the M-extrapolation, and we study their correctness. Our experiments show an overall decrease of the computation time and, most importantly, allow termination of some previously unsolvable benchmarks.