Decidable first-order transition logics for PA-processes

DOI10.1016/j.ic.2005.02.003zbMath1101.68683MaRDI QIDQ2575856

Denis Lugiez, Philippe Schnoebelen

Publication date: 7 December 2005

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2005.02.003

zbMATH Keywords

Regular tree languages; Regular model checking; Transition logics; Verification of recursive parallel systems

Mathematics Subject Classification ID

68Q60: Specification and verification (program logics, model checking, etc.)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Finite tree automata with cost functions
• Process rewrite systems.
• A structural approach to operational semantics
• Decidability of bisimulation equivalence for process generating context-free languages
• Parametric temporal logic for “model measuring”
• Process Algebra
• A really temporal logic
• Tableau methods for PA-processes
• Efficient algorithms for pre* and post* on interprocedural parallel flow graphs
• FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science
• Basic theory of feature trees
• On Context-Free Languages
• Generalized finite automata theory with an application to a decision problem of second-order logic
• Decidability of model checking with the temporal logic EF
• Symbolic model checking with rich assertional languages
• Deciding bisimulation-like equivalences with finite-state processes
• The regular viewpoint on PA-processes
• How to Parallelize sequential processes
• Infinite results