Where:

Laboratoire Spécification et Vérification

École Normale Supérieure de Cachan

61, avenue du Président Wilson

94235 Cachan CEDEX

Title:

Temporal Logic for Concurrent Recursive Programs

Description:

 
The analysis of a program that consists of a fixed number of recursive threads communicating with one another is particularly challenging, due to the usually high complexity of interaction between its components. All the more, it is important to provide tools and algorithms that support the design of correct programs, or verify if a given program corresponds to a specification.

Communication between processes can take place via shared variables or through first-in first-out channels. In this internship, we focus on the first paradigm. One model of concurrent recursive programs that communicate via shared variables (or rendez-vous) has been defined in [2]. It is centered around the notions of a Mazurkiewicz trace, which is a well-studied concept in concurrency theory [4], and visibly pushdown automata, a restricted class of pushdown automata. The aim of the internship will be to design a linear-time temporal logic (LTL) for concurrent recursive programs. This will require the combination of works on logics for sequential recursive programs and concurrent finite-state programs (cf. [1, 3]). In particular, the logic should come with several next-modalities, one for associating a call with a corresponding return, and another one for internal computations.

Contact:

 

Benedikt Bollig, Paul Gastin et Marc Zeitoun

Tél: 01 47 40 - 75 38/75 60/77 87

Email: (bollig|gastin|mz)@lsv.ens-cachan.fr

Web: http://www.lsv.ens-cachan.fr/~(bollig|gastin|zeitoun)

References

[1]

R. Alur, M. Arenas, P. Barceló, K. Etessami, N. Immerman, and L. Libkin. First-order and temporal logics for nested words. Logical Methods in Computer Science, 4(4:11):1–44, 2008.

[2]

B. Bollig, M.-L. Grindei, and P. Habermehl. Realizability of concurrent recursive programs In Proceedings of FOSSACS 2009, Lecture Notes in Computer Science, Springer, 2009. to appear.

[3]

V. Diekert and P. Gastin. LTL is expressively complete for Mazurkiewicz traces. Journal of Computer and System Sciences, 64(2):396–418, 2002.

[4]

V. Diekert and G. Rozenberg, editors. The Book of Traces. World Scientific, Singapore, 1995.

This document was translated from L^AT_EX by H^EV^EA.