TY - GEN
T1 - The linear temporal logic of rewriting maude model checker
AU - Bae, Kyungmin
AU - Meseguer, José
N1 - Acknowledgments. A considerable part of this work was carried out during a Summer internship of Kyungmin Bae at SRI’s Computer Science Laboratory. We thank Steven Eker, Mark-Oliver Stehr, and Carolyn Talcott for the very fruitful discussions, particularly on issues pertaining to the Maude’s LTL model checker, that greatly facilitated the task of developing the LTLR implementation. This work has been partially supported by NSF Grants CNS 07-16638 and CCF 09-05584.
PY - 2010
Y1 - 2010
N2 - 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.
AB - 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.
KW - Automata
KW - Maude
KW - Model checking
KW - Rewriting Logic
UR - http://www.scopus.com/inward/record.url?scp=78349265700&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=78349265700&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-16310-4_14
DO - 10.1007/978-3-642-16310-4_14
M3 - Conference contribution
AN - SCOPUS:78349265700
SN - 3642163092
SN - 9783642163098
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 208
EP - 225
BT - Rewriting Logic and Its Applications - 8th International Workshop, WRLA 2010, Held as a Satellite Event of ETAPS 2010, Revised Selected Papers
T2 - 8th International Workshop on Rewriting Logic and Its Applications, WRLA 2010, Held as a Satellite Event of ETAPS 2010
Y2 - 20 March 2010 through 21 March 2010
ER -