On decidability of LTL model checking for process rewrite systems

DOI10.1007/s00236-008-0082-3zbMath1172.68038OpenAlexW2806135590MaRDI QIDQ1006890

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

Publication date: 26 March 2009

Published in: Acta Informatica (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00236-008-0082-3

Mathematics Subject Classification ID

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

Related Items (4)

Decidable models of integer-manipulating programs with recursive parallelism ⋮ Refining the Process Rewrite Systems Hierarchy via Ground Tree Rewrite Systems ⋮ Reachability is decidable for weakly extended process rewrite systems ⋮ Model checking dynamic pushdown networks

Cites Work

• Process rewrite systems.
• First-order logic with two variables and unary temporal logic
• An Algorithm for the General Petri Net Reachability Problem
• CONCUR 2004 - Concurrency Theory
• On Decidability of LTL Model Checking for Process Rewrite Systems
• Verification, Model Checking, and Abstract Interpretation
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: On decidability of LTL model checking for process rewrite systems