参数化时态自动机中的参数更新
摘要：使用参数定时自动机（Parametric Timed Automata，简称PTAs）的新类别，允许将时钟与参数进行比较，如经典的PTAs一样，还允许将时钟更新为参数。我们在这里重点关注EF-emptiness问题：“对于某个给定的位置，某个参数估值的集合是否能够到达实例化的定时自动机为空集？”。对于PTAs来说，这个问题是无法判定的，我们的扩展也是如此。然而，如果我们每次比较时钟和参数时都更新所有的时钟，并且每次将时钟更新为参数时都更新所有的时钟，我们可以得到一个语法子类，可以判定EF-emptiness问题，甚至可以对有理估值的集合进行准确的合成，以便到达给定的位置。据我们所知，这是第一个非平凡的PTAs子类，实际上甚至还扩展了参数化更新操作，可以实现这一点。
作者：''Etienne Andr''e, Didier Lime, Mathias Ramparison
论文ID：1904.08824
分类：Formal Languages and Automata Theory
分类简称：cs.FL
提交时间：2023-06-22