Skip to Main content Skip to Navigation
Conference papers

A Temporal Logic for Multi-threaded Programs

Abstract : Temporal logics for nested words are a specification formalism for procedural programs, since they express requirements about matching calls and returns. We extend this formalism to multiply nested words, which are natural models of the computations of concurrent programs. We study both the satisfiability and the model-checking problems, when the multiply nested words are runs of multi-stack pushdown systems (Mpds). In particular, through a tableau-based construction, we define a Büchi Mpds for the models of a given formula. As expected both problems are undecidable, thus we consider some meaningful restrictions on the Mpds, and show decidability for the considered problems.
Document type :
Conference papers
Complete list of metadata

Cited literature [15 references]  Display  Hide  Download
Contributor : Hal Ifip <>
Submitted on : Tuesday, July 4, 2017 - 5:45:40 PM
Last modification on : Monday, October 19, 2020 - 8:02:03 PM
Long-term archiving on: : Friday, December 15, 2017 - 1:02:23 AM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



Salvatore Torre, Margherita Napoli. A Temporal Logic for Multi-threaded Programs. 7th International Conference on Theoretical Computer Science (TCS), Sep 2012, Amsterdam, Netherlands. pp.225-239, ⟨10.1007/978-3-642-33475-7_16⟩. ⟨hal-01556217⟩



Record views


Files downloads