# LTL Model Checking for Communicating Concurrent Programs

## Abstract

We present in this paper a new approach to the static analysis of concurrent programs with procedures. To this end, we model multi-threaded programs featuring recursive procedure calls and synchronisation by rendez-vous between parallel threads with communicating pushdown systems (from now on CPDSs). The reachability problem for this particular class of automata is unfortunately undecidable. However, it has been shown that an efficient abstraction of the execution traces language can nonetheless be computed. To this end, an algebraic framework to over-approximate context-free languages has been introduced by Bouajjani et al. In this paper, we combine this framework with an automata-theoretic approach in order to approximate an answer to the model checking problem of the linear-time temporal logic (from now on LTL) on CPDSs. We then present an algorithm that, given a single-indexed or emphstutter-invariant LTL formula, allows us to prove that no run of a CPDS verifies this formula if the procedure ends.

## Bibtex (lrde.bib)

@Article{	  pommellet.20.isse,
author	= {Adrien Pommellet and Tayssir Touili},
title		= {LTL Model Checking for Communicating Concurrent Programs},
journal	= {Innovations in Systems and Software Engineering: a NASA
journal (ISSE)},
year		= 2020,
volume	= {??},
number	= {??},
pages		= {??--??},
month		= jun,
publisher	= {Springer},
abstract	= {We present in this paper a new approach to the static
analysis of concurrent programs with procedures. To this
end, we model multi-threaded programs featuring recursive
procedure calls and synchronisation by rendez-vous between
parallel threads with \emph{communicating pushdown systems}
(from now on CPDSs).

The reachability problem for this particular class of
automata is unfortunately undecidable. However, it has been
shown that an efficient abstraction of the execution traces
language can nonetheless be computed. To this end, an
algebraic framework to over-approximate context-free
languages has been introduced by Bouajjani et al.

In this paper, we combine this framework with an
automata-theoretic approach in order to approximate an
answer to the model checking problem of the
\emph{linear-time temporal logic} (from now on LTL) on
CPDSs. We then present an algorithm that, given a
\emph{single-indexed} or \emph{stutter-invariant} LTL
formula, allows us to prove that no run of a CPDS verifies
this formula if the procedure ends.},
doi		= {10.1007/s11334-020-00363-6}
}