The Linear Temporal Logic of Rewriting Maude Model Checker

DOI10.1007/978-3-642-16310-4_14MaRDI QIDQ4933287zbMATH OpenOpenAlexFDO

Authors Kyungmin Bae, José Meseguer

Publication date 12 October 2010

Published in Rewriting Logic and Its Applications (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-16310-4_14

zbMATH Keywords

automataMaudemodel checkingrewriting logic

Mathematics Subject Classification ID

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

Recommendations

• A rewriting-based model checker for the linear temporal logic of rewriting
• A model checker for linear time temporal logic
• scientific article; zbMATH DE number 1982209
• The Maude LTL model checker
• Model checking general linear temporal logic
• Model checking linear coalgebraic temporal logics: an automata-theoretic approach
• Linear temporal logic symbolic model checking
• scientific article; zbMATH DE number 1487477
• An expressively complete linear time temporal logic for Mazurkiewicz traces
• A simple rewrite system for the normalization of linear temporal logic

Cited in

(13)

• Twenty years of rewriting logic
• Strategies, model checking and branching-time properties in Maude
• Egalitarian State-Transition Systems
• The Maude LTL model checker
• From linear temporal logic properties to rewrite propositions
• Infinite-state model checking of LTLR formulas using narrowing
• Model checking LTLR formulas under localized fairness
• The Temporal Logic of Rewriting: A Gentle Introduction
• scientific article; zbMATH DE number 1982209 (Why is no real title available?)
• Compositional specification in rewriting logic
• A rewriting-based model checker for the linear temporal logic of rewriting
• Model checking TLR* guarantee formulas on infinite systems
• A simple rewrite system for the normalization of linear temporal logic

Describes a project that uses

Uses Software

• LTL2BA
• MAGIC
• Maude

This page was built for publication: The Linear Temporal Logic of Rewriting Maude Model Checker

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