Minimal-time synthesis for parametric timed automata

Étienne André, Vincent Bloemen*, Laure Petrucci, Jaco van de Pol

*Corresponding author for this work

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

1 Citation (Scopus)
18 Downloads (Pure)

Abstract

Parametric timed automata (PTA) extend timed automata by allowing parameters in clock constraints. Such a formalism is for instance useful when reasoning about unknown delays in a timed system. Using existing techniques, a user can synthesize the parameter constraints that allow the system to reach a specified goal location, regardless of how much time has passed for the internal clocks. We focus on synthesizing parameters such that not only the goal location is reached, but we also address the following questions: what is the minimal time to reach the goal location? and for which parameter values can we achieve this? We analyse the problem and present a semi-algorithm to solve it. We also discuss and provide solutions for minimizing a specific parameter value to still reach the goal. We empirically study the performance of these algorithms on a benchmark set for PTAs and show that minimal-time reachability synthesis is more efficient to compute than the standard synthesis algorithm for reachability. Data or code related to this paper is available at: [26].

Original languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems
Subtitle of host publication25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings
EditorsLijun Zhang, Tomáš Vojnar
Place of PublicationCham
PublisherSpringer
Pages211-228
Number of pages18
ISBN (Electronic)978-3-030-17464-4
ISBN (Print)978-3-030-17465-1
DOIs
Publication statusPublished - 1 Jan 2019
Event25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019 - Charles University, Prague, Czech Republic
Duration: 6 Apr 201911 Apr 2019
Conference number: 25

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume11428
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349
NameTheoretical Computer Science and General Issues
PublisherSpringer

Conference

Conference25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019
Abbreviated titleTACAS 2019
CountryCzech Republic
CityPrague
Period6/04/1911/04/19
Otherheld as part of the 22nd European Joint Conferences on Theory and Practice of Software, ETAPS 2019

Fingerprint Dive into the research topics of 'Minimal-time synthesis for parametric timed automata'. Together they form a unique fingerprint.

  • Cite this

    André, É., Bloemen, V., Petrucci, L., & van de Pol, J. (2019). Minimal-time synthesis for parametric timed automata. In L. Zhang, & T. Vojnar (Eds.), Tools and Algorithms for the Construction and Analysis of Systems: 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings (pp. 211-228). (Lecture Notes in Computer Science; Vol. 11428), (Theoretical Computer Science and General Issues). Cham: Springer. https://doi.org/10.1007/978-3-030-17465-1_12