最大加线性系统的形式分析与验证
摘要：Max-Plus线性（MPL）系统在交通网络、制造业和生物系统等实际应用中具有代数形式。本文探讨了自动分析MPL属性的问题，考虑了结构性属性（如瞬态和循环性）和用户定义的时间性属性的开放问题。我们提出了时间差异LTL（TDLTL），一种涵盖了由MPL系统控制的离散时间事件之间的延迟的逻辑，并且对于在MPL上模型检查TDLTL进行了问题描述。首先，我们考虑了基于无穷状态转换系统的验证框架，并提出了基于模型检查编码的方法。然后，我们利用MPL系统的特定特性，设计了一个基于可满足性模型理论（SMT）的高度优化的组合方法。我们对大量基准进行了实验评估所提出方法的特性。结果表明，所提方法在表达性和效果上明显优于现有竞争对手，并展示了组合方法相对于归约到模型检查的优势。
作者：Muhammad Syifa'ul Mufid, Andrea Micheli, Alessandro Abate, Alessandro Cimatti
论文ID：2308.10587
分类：Formal Languages and Automata Theory
分类简称：cs.FL
提交时间：2023-08-22