Temporal logics for concurrent recursive programs: satisfiability and model checking

DOI10.1016/j.jal.2014.05.001zbMath1310.68142OpenAlexW2082577494MaRDI QIDQ472794

Benedikt Bollig, Aiswarya Cyriac, Paul Gastin, Marc Zeitoun

Publication date: 20 November 2014

Published in: Journal of Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jal.2014.05.001

zbMATH Keywords

model checkingtemporal logicsatisfiabilityconcurrent recursive programsMazurkiewicz tracesnested words

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) Temporal logic (03B44) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (3)

Realizability of concurrent recursive programs ⋮ The complexity of model checking multi-stack systems ⋮ Reachability of scope-bounded multistack pushdown systems

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Pure future local temporal logics are expressively complete for Mazurkiewicz traces
• Uniform satisfiability problem for local temporal logics over Mazurkiewicz traces
• Propositional dynamic logic of regular programs
• Propositional Dynamic Logic for Message-Passing Systems
• Global Model Checking of Ordered Multi-Pushdown Systems
• MSO Decidability of Multi-Pushdown Systems via Split-Width
• Alternation Elimination for Automata over Nested Words
• Temporal Logics for Concurrent Recursive Programs: Satisfiability and Model Checking
• Reachability of Multistack Pushdown Systems with Scope-Bounded Matching Relations
• Adding nesting structure to words
• Emptiness of Multi-pushdown Automata Is 2ETIME-Complete
• PDL with intersection and converse: satisfiability and infinite-state model checking
• Realizability of Concurrent Recursive Programs
• First-Order and Temporal Logics for Nested Words
• On Communicating Finite-State Machines
• Notes on finite asynchronous automata
• Tools and Algorithms for the Construction and Analysis of Systems
• Logics for Unranked Trees: An Overview
• Computational Complexity
• The tree width of auxiliary storage
• Context-Bounded Analysis of Concurrent Queue Systems
• 2-Exp Time lower bounds for propositional dynamic logics with intersection
• MULTI-PUSH-DOWN LANGUAGES AND GRAMMARS
• Tools and Algorithms for the Construction and Analysis of Systems
• Propositional Dynamic Logic with Converse and Repeat for Message-Passing Systems
• CONCUR 2003 - Concurrency Theory

This page was built for publication: Temporal logics for concurrent recursive programs: satisfiability and model checking