@inproceedings{7779227b2e94415084cf3306a6d35553,
title = "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 event-related 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.",
keywords = "Automata, Maude, Model checking, Rewriting Logic",
author = "Kyungmin Bae and Jos{\'e} Meseguer",
year = "2010",
month = nov,
day = "22",
doi = "10.1007/978-3-642-16310-4_14",
language = "English (US)",
isbn = "3642163092",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "208--225",
booktitle = "Rewriting Logic and Its Applications - 8th International Workshop, WRLA 2010, Held as a Satellite Event of ETAPS 2010, Revised Selected Papers",
note = "8th International Workshop on Rewriting Logic and Its Applications, WRLA 2010, Held as a Satellite Event of ETAPS 2010 ; Conference date: 20-03-2010 Through 21-03-2010",
}