一句话：证明参数化时间自动机的无时间语言与迹保持问题一般不可判定，并给出若干可判定子类及鲁棒变体。
参数化时间自动机（PTA）是建模含未知时间延迟的并发系统的强有力形式化工具。本文研究无时间语言保持与迹保持问题：给定一个参考参数取值，是否存在另一个参数取值，使两者具有相同的无时间语言，或相同的迹集合。作者证明这些问题对一般 PTA 以及受限的 L/U-PTA 均不可判定，即使参数仅取整数值或时间有界时也如此。另一方面，他们给出若干可判定子类：单时钟 PTA，以及单参数的确定性 L-PTA 与 U-PTA。文章还考虑了这些问题的鲁棒版本，额外要求从参考取值到新取值之间的所有取值都保持该语言。
Parametric timed automata (PTA) are a powerful formalism to model and reason about concurrent systems with some unknown timing delays. In this paper, we address the (untimed) language- and trace-preservation problems: given a reference parameter valuation, does there exist another parameter valuation with the same untimed language, or with the same set of traces? We show that these problems are undecidable both for general PTA and for the restricted class of L/U-PTA, even for integer-valued parameters, or over bounded time. On the other hand, we exhibit decidable subclasses: 1-clock PTA, and 1-parameter deterministic L-PTA and U-PTA. We also consider robust versions of these problems, where we additionally require that the language be preserved for all valuations between the reference valuation and the new valuation. Comment: Extended version of the paper of the name published in the proceedings of FORMATS 2015
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{AndreLM19,
title = {Language Preservation Problems in Parametric Timed Automata},
author = {Étienne André and Didier Lime and Nicolas Markey},
journal = {Logical Methods in Computer Science},
volume = {Volume 16, Issue 1},
year = {2020},
doi = {10.23638/lmcs-16(1:5)2020}
}