Model Checking TLR* Guarantee Formulas on Infinite Systems

DOI10.1007/978-3-642-54624-2_7zbMath1407.68296OpenAlexW1508941494WikidataQ123905825 ScholiaQ123905825MaRDI QIDQ5403070

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

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

strategymodel checkingtemporal logicrewriting logicMaudecache coherenceinfinite-state systemguarantee formulaTLR*

Mathematics Subject Classification ID

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

Related Items (3)

Compositional Specification in Rewriting Logic ⋮ Strategies, model checking and branching-time properties in Maude ⋮ Egalitarian State-Transition Systems

Uses Software

• Maude

Cites Work

• Equational abstractions
• 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
• Semantic foundations for generalized rewrite theories
• A Survey of Rewriting Strategies in Program Transformation Systems
• Abstract Logical Model Checking of Infinite-State Systems Using Narrowing
• Model Checking LTLR Formulas under Localized Fairness
• Algebraic laws for nondeterminism and concurrency
• The Linear Temporal Logic of Rewriting Maude Model Checker
• A Rewriting-Based Model Checker for the Linear Temporal Logic of Rewriting
• Symbolic Model Checking of Infinite-State Systems Using Narrowing
• Well-structured transition systems everywhere!

This page was built for publication: Model Checking TLR* Guarantee Formulas on Infinite Systems