Model checking TLR* guarantee formulas on infinite systems

DOI10.1007/978-3-642-54624-2_7MaRDI QIDQ5403070zbMATH OpenOpenAlexWikidataFDO

Authors Óscar Martín, Alberto Verdejo, Narciso Martí-Oliet

Publication date 25 March 2014

Published in Specification, Algebra, and Software (Search for Journal in Brave)

Full work available at URL https://eprints.ucm.es/22647/1/master_thesis_-_two_sides_-_for_printing.pdf

zbMATH Keywords

cache coherenceguarantee formulainfinite-state systemMaudemodel checkingrewriting logicstrategytemporal logicTLR*

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• A rewriting-based model checker for the linear temporal logic of rewriting
• The Maude LTL model checker
• Infinite-state model checking of LTLR formulas using narrowing
• The Linear Temporal Logic of Rewriting Maude Model Checker
• scientific article; zbMATH DE number 1982209

Cites work

• A rewriting-based model checker for the linear temporal logic of rewriting
• A survey of rewriting strategies in program transformation systems
• Abstract logical model checking of infinite-state systems using narrowing
• Algebraic laws for nondeterminism and concurrency
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Conditional rewriting logic as a unified model of concurrency
• ELAN from a rewriting logic point of view
• Equational abstractions
• Model checking LTLR formulas under localized fairness
• Semantic foundations for generalized rewrite theories
• Symbolic Model Checking of Infinite-State Systems Using Narrowing
• The Linear Temporal Logic of Rewriting Maude Model Checker
• Well-structured transition systems everywhere!

Cited in

(5)

• Strategies, model checking and branching-time properties in Maude
• Egalitarian State-Transition Systems
• The Maude LTL model checker
• scientific article; zbMATH DE number 1231502 (Why is no real title available?)
• Compositional specification in rewriting logic

Describes a project that uses

Uses Software

• Maude

This page was built for publication: Model checking TLR* guarantee formulas on infinite systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5403070)