The linear temporal logic of rewriting maude model checker

Kyungmin Bae, José Meseguer

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationRewriting Logic and Its Applications - 8th International Workshop, WRLA 2010, Held as a Satellite Event of ETAPS 2010, Revised Selected Papers
Pages208-225
Number of pages18
DOIs
StatePublished - 2010
Event8th International Workshop on Rewriting Logic and Its Applications, WRLA 2010, Held as a Satellite Event of ETAPS 2010 - Paphos, Cyprus
Duration: Mar 20 2010Mar 21 2010

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6381 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other8th International Workshop on Rewriting Logic and Its Applications, WRLA 2010, Held as a Satellite Event of ETAPS 2010
Country/TerritoryCyprus
CityPaphos
Period3/20/103/21/10

Keywords

  • Automata
  • Maude
  • Model checking
  • Rewriting Logic

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'The linear temporal logic of rewriting maude model checker'. Together they form a unique fingerprint.

Cite this