参数化时态自动机中的语言保持问题
摘要：参数化时态自动机（PTA）是一种强大的形式化工具，用于建模和推理并发系统中的一些未知时间延迟。本文解决了（非时态的）语言和轨迹保持问题：给定一个参考参数赋值，是否存在另一个参数赋值具有相同的非时态语言或相同的轨迹集合？我们证明这些问题对于一般的PTA和受限的L/U-PTA都是不可判定的，即使对于整数值参数或有界时间而言也是如此。另一方面，我们展示了可判定的子类：1钟表PTA，以及1参数确定性L-PTA和U-PTA。我们还考虑了这些问题的强健版本，其中我们额外要求语言在参考赋值和新赋值之间的所有赋值中都得到保持。
作者：''Etienne Andr''e, Didier Lime and Nicolas Markey
论文ID：1807.07091
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22