Infinite-state model checking of LTLR formulas using narrowing

DOI10.1007/978-3-319-12904-4_6MaRDI QIDQ2945133zbMATH OpenOpenAlexFDO

Authors Kyungmin Bae, José Meseguer

Publication date 9 September 2015

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

Full work available at URL https://doi.org/10.1007/978-3-319-12904-4_6

zbMATH Keywords

infinite-state systemsLTLRmodel checkingnarrowing

Mathematics Subject Classification ID

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

Recommendations

• Abstract logical model checking of infinite-state systems using narrowing
• A rewriting-based model checker for the linear temporal logic of rewriting
• The Linear Temporal Logic of Rewriting Maude Model Checker
• Symbolic Model Checking of Infinite-State Systems Using Narrowing
• The Temporal Logic of Rewriting: A Gentle Introduction

Cited in

(14)

• Sentence-normalized conditional narrowing modulo in rewriting logic and Maude
• Generalized rewrite theories, coherence completion, and symbolic methods
• Programming and symbolic computation in Maude
• An Asymptotically Correct Finite Path Semantics for LTL
• Sentence-Normalized Conditional Narrowing Modulo in Rewriting Logic and Maude
• Liveness properties in CafeOBJ -- a case study for meta-level specifications
• Abstract logical model checking of infinite-state systems using narrowing
• Infinite-state liveness-to-safety via implicit abstraction and well-founded relations
• Variant-Based Satisfiability in Initial Algebras
• A rewriting-based model checker for the linear temporal logic of rewriting
• Model checking TLR* guarantee formulas on infinite systems
• Symbolic Model Checking of Infinite-State Systems Using Narrowing
• A rewriting-logic-with-SMT-based formal analysis and parameter synthesis framework for parametric time Petri nets
• DM-check: verifying invariants of concurrent systems by deductive model checking

This page was built for publication: Infinite-state model checking of LTLR formulas using narrowing

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