A Rewriting-Based Model Checker for the Linear Temporal Logic of Rewriting

被引：11

作者：

Bae, Kyungmin ^{[1
]}

Meseguer, Jose ^{[1
]}

机构：

[1] Univ Illinois, Dept Comp Sci, Urbana, IL 61801 USA

来源：

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE | 2012年 / 290卷

关键词：

temporal logic of rewriting; model checking; rewriting logic; reflective transformation;

D O I：

10.1016/j.entcs.2012.11.009

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

This paper presents a model checker for LTLR, a subset of the temporal logic of rewriting TLR* extending linear temporal logic with spatial action patterns. Both LTLR and TLR* are very expressive logics generalizing well- known state- based and action- based logics. Furthermore, the semantics of TLR* is given in terms of rewrite theories, so that the concurrent systems on which the LTLR properties are model checked can be specified at a very high level with rewrite rules. This paper answers a nontrivial challenge, namely, to be able to build a model checker to model check LTLR formulas on rewrite theories with relatively little effort by reusing Maude's LTL model checker for rewrite theories. For this, the reflective features of both rewriting logic and its Maude implementation have proved extremely useful.

引用

页码：19 / 36

页数：18

共 37 条

[1]

Bae K., 2008, TLR MODEL CHECKER SO

[2]

Beek M., 2008, P FMICS IN PRESS

[3] Semantic foundations for generalized rewrite theories [J].