论文标题
高维最大线性系统的符号达到性分析
Symbolic Reachability Analysis of High Dimensional Max-Plus Linear Systems
论文作者
论文摘要
这项工作讨论了最大值线性（MPL）系统的可及性分析（RA），这是一类连续空间，离散事件模型，这些模型定义在最大值代数上。鉴于初始目标和目标集，我们开发算法来验证MPL系统是否存在从初始组开始，最终到达目标集的轨迹。我们表明，可以通过编码MPL系统以及初始目标和目标设置为差异逻辑来象征性地求解RA，然后通过现成的可满足性模型理论（SMT）求解器检查所得逻辑公式的满意度。显示开发的基于SMT的算法的性能和可扩展性清楚地超过了MPL系统的最先进的RA算法，新允许研究高维MPL系统的RA：对具有100多种连续变量的模型的验证，显示了这些技术对工业相关性MPL系统的适用性。
This work discusses the reachability analysis (RA) of Max-Plus Linear (MPL) systems, a class of continuous-space, discrete-event models defined over the max-plus algebra. Given the initial and target sets, we develop algorithms to verify whether there exist trajectories of the MPL system that, starting from the initial set, eventually reach the target set. We show that RA can be solved symbolically by encoding the MPL system, as well as initial and target sets into difference logic, and then checking the satisfaction of the resulting logical formula via an off-the-shelf satisfiability modulo theories (SMT) solver. The performance and scalability of the developed SMT-based algorithms are shown to clearly outperform state-of-the-art RA algorithms for MPL systems, newly allowing to investigate RA of high-dimensional MPL systems: the verification of models with more than 100 continuous variables shows the applicability of these techniques to MPL systems of industrial relevance.
