Efficient Convex Zone Merging in Parametric Timed Automata

Étienne André, Dylan Marinho, Laure Petrucci, Jaco van de Pol

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

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.

Original languageEnglish
Title of host publicationFormal Modeling and Analysis of Timed Systems - 20th International Conference, FORMATS 2022, Proceedings
EditorsSergiy Bogomolov, David Parker
PublisherSpringer Science and Business Media Deutschland GmbH
Pages200-218
Number of pages19
ISBN (Print)9783031158384
DOIs
Publication statusPublished - 1 Jan 2022
Externally publishedYes
Event20th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2022 - Warsaw, Poland
Duration: 13 Sept 202215 Sept 2022

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume13465 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference20th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2022
Country/TerritoryPoland
CityWarsaw
Period13/09/2215/09/22

Fingerprint

Dive into the research topics of 'Efficient Convex Zone Merging in Parametric Timed Automata'. Together they form a unique fingerprint.

Cite this