Our objective is to fundamentally understand how strong synchrony and
true concurrency are related, and how one can transform a system of the
one class into a system of the other one. This work has several facets:
how to make an executable synchronous program compliant with the
paradigm of true concurrency, in which the model of communication is
simply that of a send/receive mechanism, which guarantees message
losslessness and order preservation, but does not require any kind of
global synchrony?
conversely, given a program obeying the paradigm of true
concurrency, how can one make it looking like a perfectly synchronous
program?
The first point is addressed in task 4.1 (code distribution), here we
concentrate on the second one. We first recognized that this point
amounts to constructing a suitable dating function, compatible
with the partial ordering of events in the considered program. Thus we
concentrated on this problem of dating, and this resulted in a new,
comprehensive way, to manipulate dating for synchronous and truly
asynchronous programs using a new symbolic algebra generalizing the
MaxPlus linear algebra introduced by Cohen and Quadrat in the
eighties for timed event graphs.
Achieved Results:
In this work, we propose an extension of so-called MaxPlus algebraic
techniques to handle more realistic types of real-time systems. In
particular, our framework encompasses timed Petri Nets (with otherwise
no restriction), graph or partial order automata, and more generally
abstract models of real-time computations (including synchronous programs
running over distributed architectures).
To achieve this, we propose a new
dioid of formal power series a la Kleene-Schutzenberger, which has
both 1/ formal power series corresponding to regular languages, and 2/
MaxPlus power series associated to timed event graphs by Cohen and
Quadrat, as
subcases.
We provide the associated linear algebraic setting, together with
a graphical notation for corresponding systems.
Finally we sketch how this
framework can be used to symbolically solve several problems of
interest,
related to real-time systems.
No tool is available yet, implementing these ideas.
Publications:
A. Benveniste, C. Jard, and S. Gaubert
MaxPlus techniques for timed systems (DRAFT) manuscript, October 1997