Where:

Laboratoire Spécification et Vérification

École Normale Supérieure de Cachan

61, avenue du Président Wilson

94235 Cachan CEDEX

Title:

Synthesis of Distributed Real-Time Systems

Description:

 
Timed automata are a well-studied formalism to describe reactive systems that come with timing constraints. When modeling distributed real-time systems where several components communicate with one another, one usually assumes that the time of any local component evolves according to a global clock that it shares with all other components. A local clock, however, often depends on several external factors such as temperature and workload so that it might evolve differently from other local clocks. Recently, a model of distributed real-time systems has been proposed, which takes into account that local clocks may run at different speed [1].

As the precise evolution of local clock rates is often too complex or even unknown, the model comes with several semantics. The existential semantics exhibits all those behaviors that are possible under some time evolution. The universal semantics captures only those behaviors that are possible under all time evolutions. While emptiness and universality of the universal semantics are in general undecidable, the existential semantics is always regular and offers a way to check a given system against safety properties. A decidable underapproximation of the universal semantics, called reactive semantics, is introduced to check a system for liveness properties.

During the internship, the synthesis problem should be studied: For which (global) specifications S, say, given as a regular word language, can we generate a distributed timed system A (over some given system architecture) such that the reactive semantics of A equals L( S)? In this context, it will be favorable to have partial-order based specification languages and a partial-order semantics for distributed timed systems.

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]

S. Akshay, Benedikt Bollig, Paul Gastin, Madhavan Mukund, and K. Narayan Kumar. Distributed timed automata with independently evolving clocks. In Proceedings of the 19th International Conference on Concurrency Theory (CONCUR'08), volume 5201 of Lecture Notes in Computer Science, pages 82–97, 2008. Springer.

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