Temporal logics for concurrent recursive programs: satisfiability and model checking
type: Item
instance of: scholarly article
title: Temporal logics for concurrent recursive programs: satisfiability and model checking
zbMATH Open document ID: 1310.68142
author: Benedikt Bollig
author: Aiswarya Cyriac
author: Paul Gastin
author: Marc Zeitoun
published in: Journal of Applied Logic
publication date: 2014-11-20T00:00:00Z
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 03B44
Mathematics Subject Classification ID: 68N30
Mathematics Subject Classification ID: 68Q85
zbMATH DE Number: 6371450
zbMATH Keywords: temporal logic
zbMATH Keywords: concurrent recursive programs
zbMATH Keywords: nested words
zbMATH Keywords: Mazurkiewicz traces
zbMATH Keywords: satisfiability
zbMATH Keywords: model checking
MaRDI profile type: Publication
full work available at URL: j.jal.2014.05.001
OpenAlex ID: W2082577494
cites work: Adding nesting structure to words
cites work: Tools and Algorithms for the Construction and Analysis of Systems
cites work: First-Order and Temporal Logics for Nested Words
cites work: Computational Complexity
cites work: Global model checking of ordered multi-pushdown systems
cites work: Emptiness of Multi-pushdown Automata Is 2ETIME-Complete
cites work: Realizability of Concurrent Recursive Programs
cites work: Propositional dynamic logic for message-passing systems
cites work: Temporal Logics for Concurrent Recursive Programs: Satisfiability and Model Checking
cites work: On Communicating Finite-State Machines
cites work: MULTI-PUSH-DOWN LANGUAGES AND GRAMMARS
cites work: Q3336675
cites work: MSO Decidability of Multi-Pushdown Systems via Split-Width
cites work: Alternation Elimination for Automata over Nested Words
cites work: Pure future local temporal logics are expressively complete for Mazurkiewicz traces
cites work: Propositional dynamic logic of regular programs
cites work: CONCUR 2003 - Concurrency Theory
cites work: Uniform satisfiability problem for local temporal logics over Mazurkiewicz traces
cites work: PDL with intersection and converse: satisfiability and infinite-state model checking
cites work: Reachability of Multistack Pushdown Systems with Scope-Bounded Matching Relations
cites work: Context-Bounded Analysis of Concurrent Queue Systems
cites work: 2-Exp Time lower bounds for propositional dynamic logics with intersection
cites work: Logics for Unranked Trees: An Overview
cites work: The tree width of auxiliary storage
cites work: Propositional dynamic logic with converse and repeat for message-passing systems
cites work: Q4298260
cites work: Q3740223
cites work: Q4219045
cites work: Notes on finite asynchronous automata
DOI: 10.1016/J.JAL.2014.05.001
description: scientific article; zbMATH DE number 6371450