A Rewriting-Based Model Checker for the Linear Temporal Logic of Rewriting

DOI10.1016/j.entcs.2012.11.009zbMath1291.68244OpenAlexW2151284417WikidataQ113318033 ScholiaQ113318033MaRDI QIDQ5166636

José Meseguer, Kyungmin Bae

Publication date: 27 June 2014

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2012.11.009

zbMATH Keywords

model checkingrewriting logicreflective transformationtemporal logic of rewriting

Mathematics Subject Classification ID

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

Related Items (9)

Model Checking Reconfigurable Petri Nets with Maude ⋮ Comparing three coordination models: Reo, ARC, and PBRD ⋮ Twenty years of rewriting logic ⋮ Compositional Specification in Rewriting Logic ⋮ A Spatial Logic for Simplicial Models ⋮ Model Checking TLR* Guarantee Formulas on Infinite Systems ⋮ Enabling synchronous and asynchronous communications in CSP for SOC ⋮ Unnamed Item ⋮ Egalitarian State-Transition Systems

Uses Software

• SLMC
• Maude
• COWS
• UNITY
• MAGIC

Cites Work

• A state/event-based model-checking approach for the analysis of abstract system properties
• Results on the propositional \(\mu\)-calculus
• The rewriting logic semantics project
• Maude's module algebra
• 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
• Maude: specification and programming in rewriting logic
• Equational rules for rewriting logic
• A spatial logic for concurrency. II
• A spatial logic for concurrency. I
• Concurrent software verification with states, events, and deadlocks
• Semantic foundations for generalized rewrite theories
• A Verification Logic for Rewriting Logic
• The Temporal Logic of Rewriting: A Gentle Introduction
• Algebraic laws for nondeterminism and concurrency
• Foundations of Software Science and Computation Structures
• Symbolic Model Checking of Logics with Actions
• State/Event Software Verification for Branching-Time Specifications
• Automated Deduction – CADE-19
• Integrated Formal Methods
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A Rewriting-Based Model Checker for the Linear Temporal Logic of Rewriting