| 摘要: |
| 基本并行进程是一个用于描述和分析并发程序的模型，是Petri网的一个重要子类.EG逻辑是一种在Hennessy-Milner Logic的基础上增加EG算子的分支时间逻辑，其中的AF算子表示从当前的状态出发性质最终会被满足，因此EG逻辑是能够表达活性的逻辑.然而，基于基本并行进程的EG逻辑的模型检测问题是不可判定的.由此，提出了基本并行进程上EG逻辑的限界模型检测方法.首先给出了基本并行进程上EG逻辑的限界语义，然后采用基于约束的方法，将基本并行进程上EG逻辑的限界模型检测问题转化为线性整数算术公式的可满足性问题，最后利用SMT求解器进行求解. |
| 关键词: 基本并行进程 限界模型检测 活性 线性整数算术 SMT求解 |
| DOI：10.13328/j.cnki.jos.005959 |
| 分类号: |
| 基金项目:国家自然科学基金（61872232，61732013） |
|
| Bounded Model Checking Liveness on Basic Parallel Processes |
|
TAN Jin-Hao, LI Guo-Qiang
|
|
School of Software, Shanghai Jiao Tong University, Shanghai 200240, China
|
| Abstract: |
| Basic parallel process (BPP) is a model for describing and analyzing concurrent programs, which is an important subclass of Petri nets. The logic EG is a branching time logic obtained by extending Hennessy-Milner Logic with the EG operator, in which the AF operator means that a certain property will be satisfied eventually from the current state. Hence, the logic EG is a logic that can express liveness. However, model checking the logic EG over BPP is undecidable. This study proposes an algorithm for the problem of bounded model checking EG over BPP. First, a bounded semantics of EG over BPP is proposed. Then, according to the constraint-based approach, a reduction from the problem of bounded model checking EG over BPP to the satisfiability problem of linear integer arithmetic formulas is given. Finally, the linear integer arithmetic formulas are solved by SMT solvers. |
| Key words: basic parallel process bounded model checking liveness linear integer arithmetic SMT solving |
