基于 ASP 及稳定失败语义的 CSP 模型检测

• 作者: 左贵征 赵岭忠
• 来源期刊: 桂林电子科技大学学报
• 学科: 工学
• 关键词: 通信顺序进程 线性时态逻辑 稳定失败语义 回答集程序设计
• 年，卷（期）: 2015,（5）
• 页码范围: 401-407
• 页数: 7页
• 分类号: TP311
• 字数: 4943字
• 语种: 中文

摘要

针对现有模型检测工具对活性描述不足、模型转换复杂,提出一种基于 ASP 及稳定失败语义的 CSP 模型检测方法。该方法采用时态逻辑 LTL 刻画性质,将进程的稳定失败模型和 LTL 公式转化为 ASP,利用 ASP 求解器验证性质,实现一次运行验证多条性质。实验结果表明,该方法既扩大了基于稳定失败模型的活性验证范围,也避免了不同模型之间的转换。

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	赵岭忠	桂林电子科技大学计算机科学与工程学院	64	229	8.0	11.0
2	左贵征	桂林电子科技大学计算机科学与工程学院	1	1	1.0	1.0