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

DOI10.1016/J.ENTCS.2009.05.033MaRDI QIDQ5179053zbMATH OpenOpenAlexFDO

Authors 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

model checkingdecidabilitylinear temporal logicinfinite-state systemsrewrite systems

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25) Temporal logic (03B44) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• On decidability of LTL model checking for process rewrite systems
• On Decidability of LTL Model Checking for Process Rewrite Systems
• Model checking for process rewrite systems and a class of action-based regular properties
• Verification, Model Checking, and Abstract Interpretation
• scientific article; zbMATH DE number 1956570
• LTL model checking for recursive programs
• LTL on finite and process traces: complexity results and a practical reasoner
• A rewriting-based model checker for the linear temporal logic of rewriting
• LTL Generalized Model Checking Revisited

Cites work

• scientific article; zbMATH DE number 3940713 (Why is no real title available?)
• scientific article; zbMATH DE number 1263840 (Why is no real title available?)
• scientific article; zbMATH DE number 2155191 (Why is no real title available?)
• scientific article; zbMATH DE number 2087500 (Why is no real title available?)
• scientific article; zbMATH DE number 1456956 (Why is no real title available?)
• CONCUR 2004 - Concurrency Theory
• Constrained properties, semilinear systems, and Petri nets
• First-order logic with two variables and unary temporal logic
• On Decidability of LTL Model Checking for Process Rewrite Systems
• On extensions of process rewrite systems: rewrite systems with weak finite-state unit
• Process rewrite systems.
• Reachability analysis of pushdown automata: Application to model-checking
• Verification on infinite structures.
• Verification, Model Checking, and Abstract Interpretation

Cited in

(2)

• On Decidability of LTL Model Checking for Process Rewrite Systems
• On decidability of LTL model checking for process rewrite systems

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

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