The linear temporal logic of rewriting maude model checker

Kyungmin Bae; José Meseguer

doi:10.1007/978-3-642-16310-4_14

The linear temporal logic of rewriting maude model checker

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English (US)
Title of host publication	Rewriting Logic and Its Applications - 8th International Workshop, WRLA 2010, Held as a Satellite Event of ETAPS 2010, Revised Selected Papers
Pages	208-225
Number of pages	18
DOIs	https://doi.org/10.1007/978-3-642-16310-4_14
State	Published - Nov 22 2010
Event	8th International Workshop on Rewriting Logic and Its Applications, WRLA 2010, Held as a Satellite Event of ETAPS 2010 - Paphos, Cyprus Duration: Mar 20 2010 → Mar 21 2010

Publication series

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

Other

Other	8th International Workshop on Rewriting Logic and Its Applications, WRLA 2010, Held as a Satellite Event of ETAPS 2010
Country	Cyprus
City	Paphos
Period	3/20/10 → 3/21/10

Keywords

Automata
Maude
Model checking
Rewriting Logic

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1007/978-3-642-16310-4_14

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

Cite this

Bae, K., & Meseguer, J. (2010). The linear temporal logic of rewriting maude model checker. In Rewriting Logic and Its Applications - 8th International Workshop, WRLA 2010, Held as a Satellite Event of ETAPS 2010, Revised Selected Papers (pp. 208-225). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6381 LNCS). https://doi.org/10.1007/978-3-642-16310-4_14

The linear temporal logic of rewriting maude model checker. / Bae, Kyungmin; Meseguer, José.

Rewriting Logic and Its Applications - 8th International Workshop, WRLA 2010, Held as a Satellite Event of ETAPS 2010, Revised Selected Papers. 2010. p. 208-225 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6381 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Bae, K & Meseguer, J 2010, The linear temporal logic of rewriting maude model checker. in Rewriting Logic and Its Applications - 8th International Workshop, WRLA 2010, Held as a Satellite Event of ETAPS 2010, Revised Selected Papers. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 6381 LNCS, pp. 208-225, 8th International Workshop on Rewriting Logic and Its Applications, WRLA 2010, Held as a Satellite Event of ETAPS 2010, Paphos, Cyprus, 3/20/10. https://doi.org/10.1007/978-3-642-16310-4_14

Bae K, Meseguer J. The linear temporal logic of rewriting maude model checker. In Rewriting Logic and Its Applications - 8th International Workshop, WRLA 2010, Held as a Satellite Event of ETAPS 2010, Revised Selected Papers. 2010. p. 208-225. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-16310-4_14

Bae, Kyungmin ; Meseguer, José. / The linear temporal logic of rewriting maude model checker. Rewriting Logic and Its Applications - 8th International Workshop, WRLA 2010, Held as a Satellite Event of ETAPS 2010, Revised Selected Papers. 2010. pp. 208-225 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@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",

}

TY - GEN

T1 - The linear temporal logic of rewriting maude model checker

AU - Bae, Kyungmin

AU - Meseguer, José

PY - 2010/11/22

Y1 - 2010/11/22

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 -