Official LSV Web Site
Concurrency in timed models.
Together with
Serge Haddad and
Patricia Bouyer, we recently focussed
on the comparison of different timed models expressing concurrency.
We have first proposed a new transformation form timed automata to time Petri nets (TPN). This
transformation allows to express additional features of timed automata (diagonal constraints,
updates to integral values), and the composition of timed automata. These results will be
published at the conference
ACSD'06.
We have then studied the relative expressiveness power (w.r.t. language acceptance) of two
classical models, namely timed automata and timed Petri nets (TdPN). We have shown that
these models coincide on finite and non-Zeno infinite words, using the introduction of read
arcs. These results will be published at the conference
ICALP'06.
Finally, we have extended Mc Millan algorithm, which computes a complete finite prefix of
the unfolding of a Petri net. Our algorithm handles the framework of netwrok of timed
automata with invariants. This framewrok induces several difficulties: first, it is in
general not an easy task to adapt partial orders methods to timed systems. Second,
it is worth noticing that because of invariants, time behaves as a global synchronization.
Our method relies partially on the previous work on timed Petri nets, but also on the feature
of read arcs, which allows us to express precisely dependencies between events. This work can
be found as a technical report of LSV.
These publications can be found on my
publication webpage .
Back to homepage