一句话：提出允许时钟更新为参数的时间自动机扩展，并找到一个可判定 EF-空问题、可精确参数综合的语法子类。
该文研究参数化时间自动机（PTA）的一种新扩展：除守卫中可将时钟与参数比较外，还允许将时钟直接更新为参数。作者关注 EF-空问题：在实例化后的时间自动机中，使给定位置可达的参数取值集合是否为空。一般 PTA 及该扩展上该问题不可判定。为此，作者引入一个语法子类：每当比较时钟与参数、以及每当将时钟更新为参数时，都更新所有时钟。在该子类上，EF-空问题可判定，并且可以对使给定位置可达的有理参数取值集合进行精确综合。据作者所知，这是首个非平凡 PTA 子类（即使扩展到参数化更新）具备该性质。
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.
@article{paperbot1315,
title = {Parametric updates in parametric timed automata},
author = {Étienne André and Didier Lime and Mathias Ramparison},
journal = {Logical Methods in Computer Science},
volume = {Volume 17, Issue 2},
year = {2021},
doi = {10.23638/lmcs-17(2:13)2021}
}