Timed Automata with Parametric Updates
Timed Automata with Parametric Updates
复制标题
具有参数更新的定时自动机
DOI：
--
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Mathias Ramparison
中科院分区：
文献类型：
--
作者：
É. André;D. Lime;Mathias Ramparison
时间自动机（TA）代表了一种强大的形式主义，可以对并发性与硬时间约束混合的系统进行建模和验证。然而，当处理不确定或未知的定时常数时，它们似乎是有限的。文献中提出了几种参数扩展，其中绝大多数导致EF-空性问题的不可判定性：“给定位置可达的赋值集是空的吗？“在这里，我们研究了TA的扩展，其中时钟可以更新为参数。虽然EF-空性问题对于有理数参数是不可判定的，但对于整数值参数则是PSPACE-完全的。此外，可以实现参数赋值集的精确合成。我们还将这两个结果扩展到EF-普适性（“是否所有的估值都使得给定的位置是可达的？“），AF-空性（“是给定位置不可避免为空的估值集合吗？“）和AF-普适性（“是否所有的估值都使得一个给定的位置是不可避免的？“）问题。
Timed automata (TAs) represent a powerful formalism to model and verify systems where concurrency is mixed with hard timing constraints. However, they can seem limited when dealing with uncertain or unknown timing constants. Several parametric extensions were proposed in the literature, and the vast majority of them leads to the undecidability of the EF-emptiness problem: "is the set of valuations for which a given location is reachable empty?" Here, we study an extension of TAs where clocks can be updated to a parameter. While the EF-emptiness problem is undecidable for rational-valued parameters, it becomes PSPACE-complete for integer-valued parameters. In addition, exact synthesis of the parameter valuations set can be achieved. We also extend these two results to the EF-universality ("are all valuations such that a given location is reachable?"), AF-emptiness ("is the set of valuations for which a given location is unavoidable empty?") and AF-universality ("are all valuations such that a given location is unavoidable?") problems.