参数化时间Petri网的成本问题
摘要：时间Petri网参数综合问题研究：带有连续演化时间变量和发射转换时离散演化的费用变量。具体而言，参数是用于转换发射时间约束的有理符号常数，我们希望综合所有的参数值，使得某个标记可达，并且成本要么是最小的，要么只需小于一个给定的界限。我们首先证明了仅存在参数值使得后一属性成立是不可判定的。尽管如此，我们提供了两个综合问题的符号半算法，并证明了它们在终止时都是正确和完整的。我们还展示了如何修改这些算法以适应参数值为整数的情况。最后，我们证明了这些修改后的版本在参数有界的情况下终止。尽管这是可以预期的，因为现在只有有限数量的可能参数值，我们的算法是符号的，因此避免了对所有参数值的显式枚举。此外，结果是表示凸多面体有限并集的符号约束，可以通过线性规划进行进一步分析。最后，我们报告了Romeo这个时间Petri网分析软件工具中该方法的实现。
作者：Didier Lime and Olivier H. Roux and Charlotte Seidner
论文ID：2109.03658
分类：Formal Languages and Automata Theory
分类简称：cs.FL
提交时间：2023-06-22