带正负速率的多价格计时自动机的可达性
形式语言与自动机理论
2024-07-26 v1
摘要
多价格计时自动机（MPTA）是具有观察变量的计时自动机，其导数可以在一个位置更改到另一个位置。观察变量是只写变量，即它们不会影响自动机的控制流程；因此 MPTA 位于计时自动机和混合自动机之间于表达力。以前的工作考虑观察变量在每个位置具有非负斜率。在本文中我们处理斜率为正和负的观察变量。我们的主要结果是为该 MPTA 变体制定一个决定性间隙可达性问题的算法。我们将间隙可达性问题翻译为混合整数-实数非线性约束系统的间隙可满足性问题。我们的主要技术贡献——一个独立的兴趣结果——是一种通过分支-界限和松弛-四舍五入组合来求解此类约束的程序。
引用
@article{arxiv.2407.18131,
title = {Reachability for Multi-Priced Timed Automata with Positive and Negative Rates},
author = {Andrew Scoones and Mahsa Shirmohammadi and James Worrell},
journal= {arXiv preprint arXiv:2407.18131},
year = {2024}
}