基于MSO逻辑的并发系统自动验证、综合与修正
计算机科学中的逻辑
2014-02-14 v1 分布式、并行与集群计算
数据结构与算法
摘要
在这项工作中，我们为五个基本问题提供了算法解决方案，这些问题涉及可由有界p/t-网建模的并发系统的验证、综合与修正。我们通过偏序来表达并发性，并假设行为规约由一元二阶逻辑给出。一个c-偏序是其哈斯图可被c条路径覆盖的偏序。对于有限的变迁集合T，我们令P(c,T,φ)表示所有满足φ的T-标记c-偏序的集合。若N=(P,T)是一个p/t-网，我们令P(N,c)表示N的所有c-偏序运行的集合。一个(b, r)-有界p/t-网是一个b-有界p/t-网，其中每个库所最多重复出现r次。我们解决以下问题：1. 验证：给定一个MSO公式φ和一个有界p/t-网N，判定是否P(N,c)⊆P(c,T,φ)，是否P(c,T,φ)⊆P(N,c)，或是否P(N,c)∩P(c,T,φ)=∅。2. 从MSO规约综合：给定一个MSO公式φ，综合一个语义最小的(b,r)-有界p/t-网N，满足P(c,T,φ)⊆P(N, c)。3. 语义最安全子系统：给定一个定义安全偏序集合的MSO公式φ，以及一个可能包含不安全行为的b-有界p/t-网N，综合一个最安全的(b,r)-有界p/t-网N'，其行为介于P(N,c)∩P(c,T,φ)与P(N,c)之间。4. 行为修复：给定两个MSO公式φ和ψ，以及一个b-有界p/t-网N，综合一个语义最小的(b,r)-有界p/t-网N'，其行为介于P(N,c) ∩ P(c,T,φ)与P(c,T,ψ)之间。5. 从契约综合：给定一个指定良好行为集合的MSO公式φ^yes和一个指定不良行为集合的MSO公式φ^no，综合一个语义最小的(b,r)-有界p/t-网N，使得P(c,T,φ^yes) ⊆ P(N,c)但P(c,T,φ^no ) ∩ P(N,c)=∅。
引用
@article{arxiv.1402.2698,
title = {Automated Verification, Synthesis and Correction of Concurrent Systems via MSO Logic},
author = {Mateus de Oliveira Oliveira},
journal= {arXiv preprint arXiv:1402.2698},
year = {2014}
}