×

zbMATH — the first resource for mathematics

The linear temporal logic of rewriting Maude model checker. (English) Zbl 1306.68099
Ölveczky, Peter Csaba (ed.), Rewriting logic and its applications. 8th international workshop, WRLA 2010, held as a satellite event of ETAPS 2010, Paphos, Cyprus, March 20–21, 2010. Revised selected papers. Berlin: Springer (ISBN 978-3-642-16309-8/pbk). Lecture Notes in Computer Science 6381, 208-225 (2010).
Summary: 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.
For the entire collection see [Zbl 1197.68017].

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
03B44 Temporal logic
68Q42 Grammars and rewriting systems
68Q45 Formal languages and automata
Software:
LTL2BA; MAGIC; Maude
PDF BibTeX XML Cite
Full Text: DOI