LTL Model Checking for Communicating Concurrent Programs

From LRDE

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 stutter-invariant LTL formula, allows us to prove that no run of a CPDS verifies this formula if the procedure ends.

Documents

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	= {16},
  number	= {2},
  pages		= {161--179},
  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 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
		  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}
}