The Maude LTL model checker

zbMATH Open1272.68243MaRDI QIDQ2851053FDOQ2851053

Authors: Steven Eker, José Meseguer, Ambarish Sridharanarayanan 

Publication date: 2 October 2013

Full work available at URL: http://www.sciencedirect.com/science/article/pii/S1571066105825344

Recommendations

• scientific article; zbMATH DE number 1982209
• Model checking TLR* guarantee formulas on infinite systems
• A rewriting-based model checker for the linear temporal logic of rewriting
• The Linear Temporal Logic of Rewriting Maude Model Checker
• Strategies, Model Checking and Branching-Time Properties in Maude

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Myths about the mutual exclusion problem
• Title not available (Why is that?)
• Title not available (Why is that?)
• Conditional rewriting logic as a unified model of concurrency
• Title not available (Why is that?)
• Title not available (Why is that?)
• Plan in Maude specifying an active network programming language
• Title not available (Why is that?)
• Title not available (Why is that?)
• An O(n log n) unidirectional distributed algorithm for extrema finding in a circle
• Title not available (Why is that?)
• Title not available (Why is that?)
• An algebraic verification of a mobile network
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (40)

• Model checking of a mobile robots perpetual exploration algorithm
• An executable semantics of clock constraint specification language and its applications
• Semantics and pragmatics of real-time maude
• The rewriting logic semantics project
• Session-based concurrency in Maude: executable semantics and type checking
• A set automaton to locate all pattern matches in a term
• Model checking TLR* guarantee formulas on infinite systems
• The Linear Temporal Logic of Rewriting Maude Model Checker
• Formal verification of complex business processes based on high-level Petri nets
• Model Checking LTL Formulae in RAISE with FDR
• Specification and analysis of the AER/NCA active network protocol suite in real-time Maude
• A rewriting-based model checker for the linear temporal logic of rewriting
• Model checking reconfigurable Petri nets with Maude
• A process calculus BigrTiMo of mobile systems and its formal semantics
• \(\mu\)-calculus model checking in Maude
• Verifying Reachability-Logic Properties on Rewriting-Logic Specifications
• Strategies, model checking and branching-time properties in Maude
• Model checking parameterized by the semantics in Maude
• An Overview of the Maude Strategy Language and its Applications
• Invariant-driven specifications in Maude
• Computer Aided Verification
• Algebraic simulations
• A rewriting semantics for ABEL with applications to hardware/software co-design and analysis
• Automated Technology for Verification and Analysis
• Metalevel transformation of strategies
• Simulating and model checking membrane systems using strategies in Maude
• Egalitarian State-Transition Systems
• Equational abstractions
• Strategies, Model Checking and Branching-Time Properties in Maude
• Maude2Lean: theorem proving for Maude specifications using Lean
• Verifiable abstractions for contract-oriented systems
• Title not available (Why is that?)
• QMaude: quantitative specification and verification in rewriting logic
• Proving VLRL action properties with the Maude model checker
• Title not available (Why is that?)
• Verification of the ROS NavFn planner using executable specification languages
• Formalization and analysis of the post-quantum signature scheme FALCON with Maude
• A language-based approach to modelling and analysis of Twitter interactions
• From hidden to visible: a unified framework for transforming behavioral theories into rewrite theories
• Bringing LTL model checking to biologists

Uses Software

• SPIN
• Maude
• LTL2BA

This page was built for publication: The Maude LTL model checker

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