PhD Thesis of Guillaume Feuillade

Version française de cette page

Subject

Logical Specifications for Petri Nets

Abstract

In practice, concurrent objects are preferred to sequential objects since for example, their realization onto distributed architectures is made easier, they bring high computational performances, etc. Automatic construction of concurrent models is then a challenging problem. This thesis investigates the synthesis (automated construction) of Petri nets from branching-time logical specifications.

Most of existing logical-based synthesis methods rely on word-automata or tree-automata to deliver a sequential object. Unfortunately extracting the concurrency inherent to the Petri models from the synthesized sequential modal is not always possible: the synthesized sequential model does not necessarily distribute properly. Then, existing algorithms do not apply in our concurrent setting anymore; incidentally decidability of this synthesis problem is an open question. This thesis first addresses decidability issues (when restricting either the class of specifications or the class of models), and second studies the narrow connections between formulas and Petri nets (e.g. logical statements for Petri net flows properties).

Committee

This thesis defense held at IRISA, December 8th 2005 with the following committee:

• Claude Jard, IRISA, ENS Cachan, (president)
• Jean-Michel Couvreur, LIFO, Université d'Orléans (referee)
• Ahmed Bouajjani LIAFA, Université Paris 7 (referee)
• Wieslaw Zielonka, LIAFA, Université Denis Diderot
• Serge Haddad, LAMSADE, Université Paris Dauphine
• Sophie Pinchinat, IRISA, Université Rennes 1 (supervisor)

Files

Thesis dissertation (pdf in French), seminar slides (pdf in French)