Sciweavers

WRLA
2010

The Linear Temporal Logic of Rewriting Maude Model Checker

13 years 9 months ago
The Linear Temporal Logic of Rewriting Maude Model Checker
Abstract. This paper presents the foundation, design, and implementation of the Linear Temporal Logic of Rewriting model checker as an extension of the Maude system. The Linear Temporal Logic of Rewriting (LTLR) extends linear temporal logic with spatial action patterns which represent rewriting events. LTLR generalizes and extends various state-based and event-based logics and aims to avoid certain types of mismatches between a system and its temporal logic properties. We have implemented the LTLR model checker at the C++ level within the Maude system by extending the existing Maude LTL model checker. Our LTLR model checker provides very expressive methods to define eventrelated properties as well as state-related properties, or, more generally, properties involving both events and state predicates. This greater expressiveness is gained without compromising performance, because the LTLR implementation minimizes the extra costs involved in handling the events of systems. Key words: Mo...
Kyungmin Bae, José Meseguer
Added 31 Jan 2011
Updated 31 Jan 2011
Type Journal
Year 2010
Where WRLA
Authors Kyungmin Bae, José Meseguer
Comments (0)