%0 Conference Proceedings
%T Parametric updates in parametric timed automata
%+ National Institute of Informatics (NII)
%+ Japanese French Laboratory for Informatics (JFLI)
%+ Laboratoire d'Informatique de Paris-Nord (LIPN)
%+ Laboratoire des Sciences du Numérique de Nantes (LS2N)
%A André, Étienne
%A Lime, Didier
%A Ramparison, Mathias
%Z Part 1: Full Papers
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 39th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE)
%C Copenhagen, Denmark
%Y Jorge A. Pérez
%Y Nobuko Yoshida
%I Springer International Publishing
%3 Formal Techniques for Distributed Objects, Components, and Syste
%V LNCS-11535
%P 39-56
%8 2019-06-17
%D 2019
%Z 1904.08824
%R 10.1007/978-3-030-21759-4_3
%Z Computer Science [cs]/Logic in Computer Science [cs.LO]
%Z Computer Science [cs]/Embedded Systems
%Z Computer Science [cs]Conference papers
%X 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.
%G English
%Z TC 6
%Z WG 6.1
%Z ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST
%2 https://hal.science/hal-02153238/document
%2 https://hal.science/hal-02153238/file/478668_1_En_3_Chapter.pdf
%L hal-02153238
%U https://hal.science/hal-02153238
%~ UNIV-NANTES
%~ INSTITUT-TELECOM
%~ UNIV-PARIS13
%~ CNRS
%~ EC-NANTES
%~ UNAM
%~ LIPN
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ USPC
%~ IFIP-FORTE
%~ LS2N
%~ LS2N-STR
%~ IFIP-DISCOTEC
%~ GALILE
%~ SORBONNE-UNIVERSITE
%~ SORBONNE-UNIV
%~ SU-SCIENCES
%~ SU-SCI
%~ UMI-3527
%~ IFIP-LNCS-11535
%~ INSTITUTS-TELECOM
%~ SORBONNE-PARIS-NORD
%~ SU-TI
%~ ANR
%~ ALLIANCE-SU
%~ NANTES-UNIVERSITE
%~ UNIV-NANTES-AV2022
%~ NU-CENTRALE