On Decidability of LTL+Past Model Checking for Process Rewrite Systems

DOI10.1016/j.entcs.2009.05.033zbMath1347.68230OpenAlexW2074884184MaRDI QIDQ5179053

Vojtěch Řehák, Jan Strejček, Mojmír Křetínský

Publication date: 19 March 2015

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.2009.05.033

zbMATH Keywords

decidabilitymodel checkinginfinite-state systemsrewrite systemslinear temporal logic

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) Decidability of theories and sets of sentences (03B25) Grammars and rewriting systems (68Q42) Temporal logic (03B44)

Cites Work

• Process rewrite systems.
• First-order logic with two variables and unary temporal logic
• CONCUR 2004 - Concurrency Theory
• On Decidability of LTL Model Checking for Process Rewrite Systems
• Verification, Model Checking, and Abstract Interpretation
• Reachability analysis of pushdown automata: Application to model-checking
• Constrained properties, semilinear systems, and Petri nets
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: On Decidability of LTL+Past Model Checking for Process Rewrite Systems