Étienne André ; Didier Lime ; Mathias Ramparison - Parametric updates in parametric timed automata

lmcs:5799 - Logical Methods in Computer Science, May 10, 2021, Volume 17, Issue 2 - https://doi.org/10.23638/LMCS-17(2:13)2021
Parametric updates in parametric timed automataArticle

Authors: Étienne André ORCID; Didier Lime ORCID; Mathias Ramparison ORCID

    We introduce a new class of Parametric Timed Automata (PTAs) where we allow clocks to be compared to parameters in guards, as in classic PTAs, but also to be updated to parameters. We focus here on the EF-emptiness problem: "is the set of parameter valuations for which some given location is reachable in the instantiated timed automaton empty?". This problem is well-known to be undecidable for PTAs, and so it is for our extension. Nonetheless, if we update all clocks each time we compare a clock with a parameter and each time we update a clock to a parameter, we obtain a syntactic subclass for which we can decide the EF-emptiness problem and even perform the exact synthesis of the set of rational valuations such that a given location is reachable. To the best of our knowledge, this is the first non-trivial subclass of PTAs, actually even extended with parametric updates, for which this is possible.


    Volume: Volume 17, Issue 2
    Published on: May 10, 2021
    Accepted on: February 5, 2021
    Submitted on: October 1, 2019
    Keywords: Computer Science - Formal Languages and Automata Theory
    Funding:
      Source : OpenAIRE Graph
    • Provable Mitigation of Side Channel through Parametric Verification; Funder: French National Research Agency (ANR); Code: ANR-19-CE25-0015
    • Parametric Analysis of Concurrent Systems; Funder: French National Research Agency (ANR); Code: ANR-14-CE28-0002

    4 Documents citing this article

    Consultation statistics

    This page has been seen 1587 times.
    This article's PDF has been downloaded 246 times.