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 (MPS). In particular, through a tableau-based construction, we define a Buchi MPS for the models of a given formula. As expected both problems are undecidable, thus we consider some meaningful restrictions on the MPS, and show decidability for the considered problems.
A Temporal Logic for Multi-threaded Programs
LA TORRE, Salvatore;NAPOLI, Margherita
2012-01-01
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 (MPS). In particular, through a tableau-based construction, we define a Buchi MPS for the models of a given formula. As expected both problems are undecidable, thus we consider some meaningful restrictions on the MPS, and show decidability for the considered problems.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
