Séminaires
Lieu
Villetaneuse: comment y aller
Cette journée était en commun avec le groupe RdP France
Programme
09h45-11h15: H-T. Nguyen, LIAFA, "Synthesis and Analysis of Product-form Petri Nets"
Abstract: For a large Markovian model, a "product form" is an explicit description of the steady-state behaviour which is otherwise generally untractable. Being first introduced in queueing networks, it has been adapted to Markovian Petri nets. Here we address three relevant issues for product-form Petri nets which were left fully or partially open:
- we provide a sound and complete set of rules for the synthesis;
- we characterise the exact complexity of classical problems like reachability;
- we introduce a new subclass for which the normalising constant (a crucial value for product-form expression) can be efficiently computed.
11h15-12h30: S. Haddad, LSV, "Modélisation et analyse des systmes à événements discrets à l'aide des réseaux de Petri récursifs"
Abstract:
Dans cet exposé nous introduirons le formalisme des réseaux de Petri récursifs. Nous étudierons ensuite quelques patrons fréquents de comportement de systèmes à événements discrets (exception, interruption et panne). Nous démontrerons la difficulté ou même l'impossibilité de modéliser ces mécanismes avec des réseaux de Petri et l'apport des réseaux de Petri récursifs. Nous terminerons cet exposé en parcourant les résultats de décidabilité et d'indécidabilité de problème standard des réseaux de Petri récursifs selon les variantes du formalisme choisi (accesibilité, model-checking, bisimulation).
12h30-14h00: Lunch
14h00-15h00: C. Dima, UPEC, "Positive and negative results for the decidability of the model-checking problem for an epistemic extension of Timed CTL"
Abstract: We present TCTLK, a continuous-time variant of the Computational Tree Logic of Knowledge, generalizing both TCTL, the continuous-time variant of CTL, and CTLK, the epistemic generalization of CTL. Formulas are interpreted over timed automata, with a synchronous and perfect recall semantics, and the observability relation requires one to specify what clocks are visible for an agent.
We show that, in general, the model-checking problem for TCTLK is undecidable even if formulas do not use any clocks Ð and hence CTLK has an undecidable model-checking problem when interpreted over timed automata. On the other hand, we show that, when each agent can see all clock values, model-checking becomes decidable.
15h00-15h30 : S. Balaguer, ENS de Cachan, "A Concurrency-Preserving Translation from Time Petri Nets to Networks of Timed Automata"
Abstract: Real-time distributed systems may be modeled in different formalisms such as time Petri nets (TPN) and networks of timed automata (NTA). This paper focuses on translating a 1-bounded TPN into an NTA and considers an equivalence which takes the distribution of actions into account. This translation is extensible to bounded TPNs. We first use S-invariants to decompose the net into components that give the structure of the automata, then we add clocks to provide the timing information. Although we have to use an extended syntax in the timed automata, this is a novel approach since the other transformations and comparisons of these models did not consider the preservation of concurrency.
Joint work with Thomas Chatain and Stefan Haar.