Where:

Laboratoire Spécification et Vérification

École Normale Supérieure de Cachan

61, avenue du Président Wilson

94235 Cachan CEDEX

Title:

Dynamic Communicating Automata

Description:

 
We study dynamic communicating automata, an automata model of programs with thread creation [1]. In a dynamic communicating automaton, there are three types of actions: (1) a new process can be created, (2) a message can be sent to an already existing process, and (3) a message can be received from an existing process. Processes can be identified by means of process variables, whose values can change dynamically during an execution of an automaton. This model extends classical communicating automata, which allow only for actions of the form (2) and (3). The semantics of both the original and the extended model is based on the notion of message sequence charts (MSCs, ITU Standard Z.120), a graphical language illustrating single program executions. Moreover, it is close to mechanisms in programming languages such as JAVA and Erlang. During the internship, one (or more) of the following problems can be studied:

1. Regular sets of MSCs have been studied in the setting of a fixed number of processes without thread creation [2]. It remains to define a robust notion of regularity that accounts for thread creation. Preferably, any regular set of MSCs should have an implementation in terms of a dynamic communicating automaton.
   
   
2. Define temporal logics for MSCs that come with a decidable model-checking problem for (a restricted class of) dynamic communicating automata.
   
   
3. Specification formalisms for MSCs with thread creation have been defined in [1, 3]. Is there a precise characterization of specifications that can be implemented as a dynamic communicating automaton without deadlock?
   
   
4. Study the relationship with other existing models such as branching automata over series-parallel pomsets [4].

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]

B. Bollig and L. Hélouët. Dynamic Communicating Automata and Dynamic MSC Grammars. Manuscript, 2009.

[2]

J. G. Henriksen, M. Mukund, K. Narayan Kumar, M. Sohoni, and P. S. Thiagarajan. A theory of regular MSC languages. Information and Computation, 202(1):1–38, 2005.

[3]

M. Leucker, P. Madhusudan, and S. Mukhopadhyay. Dynamic message sequence charts. Proceedings of 22nd Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'02), volume 2556 of Lecture Notes in Computer Science. Springer, 2002.

[4]

K. Lodaya and P. Weil.Series-parallel languages and the bounded-width property. Theoretical Computer Science, 237 (2000) 347-380.

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