论文标题
有效的凸区域合并参数定时自动机
Efficient Convex Zone Merging in Parametric Timed Automata
论文作者
论文摘要
参数定时自动机是一种有力的形式主义，用于在具有未知或不确定的时序常数的并发实时系统上推理。减少其状态空间是减少固有较大分析时间的重要方法。我们在这里介绍了基于约束（参数区域）凸结合的不同合并还原技术，从而可以减少状态数量，同时保留验证和合成结果的正确性。我们执行广泛的实验，并确定实践中最佳的启发式方法，从而在基准库上的计算时间大大减少。
Parametric timed automata are a powerful formalism for reasoning on concurrent real-time systems with unknown or uncertain timing constants. Reducing their state space is a significant way to reduce the inherently large analysis times. We present here different merging reduction techniques based on convex union of constraints (parametric zones), allowing to decrease the number of states while preserving the correctness of verification and synthesis results. We perform extensive experiments, and identify the best heuristics in practice, bringing a significant decrease in the computation time on a benchmarks library.
