Petri net synthesis

My main research activity was so far concerned with Petri net synthesis.

Petri net synthesis is an automated process which, given behavioural specifications or partial specifications of a system to be realized, decides whether the specifications are feasible, and then produces a Petri net realizing them exactly, or if this not possible produces a Petri net realizing an optimal approximation of the specifications. In the former case, the resulting Petri net system is correct by construction. Computationally efficient tools have been developed for Petri net synthesis, which may therefore play a central role in computer-assisted system design. If the specification is given by a log (set of execution traces of a process) Petri net synthesis serves as a process discovery algorithm that produces a Petri net whose language is the least Petri net language containing the given log.

... Foreword by Grzegorz Rozenberg for our book on Petri net synthesis

Active workspaces based on Guarded Attribute Grammars (GAG)

My current research activity is primarily concerned with a declarative model of data-centric collaborative systems.

The objective is to move from centralized systems using a common referential, as is common practice in business process models, to distributed systems where each participant has his own workspace that can easily be configured to meet specific needs. The dynamic evolution of a workspace depends on data and on the user-interactions. The model is thus both user centric and data driven. Users communicate by asynchronous message passing without shared memory, enabling convenient distribution.

Specifications are rule-based using Guarded Attribute Grammars.

Miscelleanous Topics

Click on the corresponding item to get more information.

• Iterative Completion of Monads
  I introduced a process of iterative completion of monads to define semantic domains as an alternative to the classical techniques of solving domain equations in complete metric spaces or complete partial orders. more
• Recognizable Event Structures
  The possibly non-distributive event domains which arise from Winskel's event structures with binary conflict are known to coincide with the domains of configurations of Stark's trace automata. We prove that whenever the transitive reduction of the order on finite elements in an event domain is a context-free graph in the sense of Müller and Schupp, the event domain may also be generated from a finite trace automaton, where both the set of states and the concurrent alphabet are finite. We show that the set of graph grammars which generate event domains is a recursive set. We obtain altogether an effective procedure which decides from an unlabeled graph grammar whether it generates an event domain and which constructs in that case a finite trace automaton recognizing that event domain. More
• Reconfigurable Workflow Systems
  We introduce a class of high level Petri nets, called reconfigurable nets, that can dynamically modify their own structure by rewriting some of their components. Boundedness of a reconfigurable net can be decided by constructing its coverability tree. Moreover such a net can be simulated by a self-modifying Petri net. The class of reconfigurable nets thus provide a subclass of self-modifying Petri nets for which boundedness can be decided. Delayed dynamic changes within workflow systems can then be handled in an extension of van der Aalst's workflow nets. For this class (the reconfigurable workflow nets), a notion of soundness has been defined that can also be verified using the coverability tree construction. More
• Petri Algebras
  The firing rule of Petri nets relies on a residuation operation for the commutative monoid of non negative integers. We identify a class of residuated commutative monoids, called Petri algebras, for which one can mimic the token game of Petri nets to define the behaviour of generalized Petri nets whose flow relations and place contents are valued in such algebraic structures. The sum and its associated residuation capture respectively how resources within places are produced and consumed through the firing of a transition. We show that Petri algebras coincide with the positive cones of lattice-ordered commutative groups and constitute the subvariety of the (duals of) residuated lattices generated by the commutative monoid of non negative integers. We however exhibit a Petri algebra whose corresponding class of nets is strictly more expressive than the class of Petri nets. More precisely, we introduce a class of nets, termed lexicographic Petri nets, that are associated with the positive cones of the lexicographic powers of the additive group of real numbers. This class of nets is universal in the sense that any net associated with some Petri algebra can be simulated by a lexicographic Petri net. All the classical decidable properties of Petri nets however (termination, covering, boundedness, structural boundedness, accessibility, deadlock, liveness ...) are undecidable on the class of lexicographic Petri nets. Finally we turn our attention to bounded nets associated with Petri algebras and show that their dynamics can be reformulated in term of MV-algebras. More
• Behavioural Contracts
  We present the modal interface theory, a unification of interface automata and modal specifications, two radically dissimilar models for interface theories. Interface automata is a game-based model, which allows the designer to express assumptions on the environment and which uses an optimistic view of composition: two components can be composed if there is an environment where they can work together. Modal specifications are a language theoretic account of a fragment of the modal \(\mu\)-calculus logic with a rich composition algebra which meets certain methodological requirements but which does not allow the environment and the component to be distinguished. The present paper contributes a more thorough unification of the two theories by correcting a first attempt in this direction by Larsen et al., drawing a complete picture of the modal interface algebra, and pushing the comparison between interface automata, modal automata and modal interfaces even further. See [1], [2], and [3].
• Opacity of Discrete Event Systems or of Artifacts
  Given a finite state system with partial observers and for each observer, a regular set of trajectories which we call a secret, we consider the question whether the observers can ever find out that a trajectory of the system belongs to some secret. We search for a regular control on the system, enforcing the specified secrets on the observers, even though they have full knowledge of this control. We show that an optimal control always exists although it is generally not regular. We state sufficient conditions for computing a finite and optimal control of the system enforcing the concurrent secret as desired. More
  I have also considered opacity of artifacts in workflow systems. A property (of an object) is opaque to an observer when he or she cannot deduce the property from its set of observations. If each observer is attached to a given set of properties (the so-called secrets), then the system is said to be opaque if each secret is opaque to the corresponding observer. Opacity has been studied in the context of discrete event dynamic systems where technique of control theory were designed to enforce opacity. This work is the first attempt to formalize opacity of artifacts in data-centric workflow systems. We motivated this problem and gave some assumptions that guarantee the decidability of opacity. Some techniques for enforcing opacity are also indicated. More
• Merging Updates in Concurrent Edition of a Document
  We consider the manipulation of hierarchically-structured documents within a complex workflow system. Such a system may consist of several subsystems distributed over a computer network. These subsystems can concurrently update partial views of the document. At some points in time we need to reconcile the various local updates by merging the partial views into a coherent global document. For that purpose, we represent the potentially-infinite set of documents compatible with a given partial view as a coinductive data structure. This set is a regular set of trees that can be obtained as the image of the partial view of the document by the canonical morphism (anamorphism) associated with a coalgebra (some kind of tree automaton). Merging partial views then amounts to computing the intersection of the corresponding regular sets of trees which can be obtained using a synchronization operation on coalgebras. More
• Attribute Grammars as Tree Transducers
  Evaluation of attributes w.r.t. an attribute grammar can be obtained by inductively computing a function expressing the dependencies of the synthesized attributes on inherited attributes. This higher-order functional approach to attribute grammars leads to a straightforward implementation using a higher-order lazy functional language like Haskell. The resulting evaluation functions are, however, not easily amenable to optimization rules. We present an alternative first-order functional interpretation of attribute grammars where the input tree is replaced with an extended cyclic tree each node of which is aware of its context viewed as an additional child tree. By the way, we demonstrate that these cyclic representations of zippers (trees with their context) are natural generalizations of doubly-linked lists to trees over an arbitrary signature. More
• Residuation of Tropical Series
  Decidability of existence, rationality of delay con- trollers and robust delay controllers are investigated for systems with time weights in the tropical and interval semirings. Depending on the (max,+) or (min,+)-rationality of the series specifying the controlled system and the control objective, cases are identified where the controller series defined by residuation is rational, and when it is positive (i.e., when delay control is feasible). When the control objective is specified by a tolerance, i.e. by two bounding rational series, a nice case is identified in which the controller series is of the same rational type as the system specification series. More
• \(\alpha\)-reconstructibility of Workflow Nets
  The process mining algorithm \(\alpha\) was introduced by van der Aalst et al. for the discovery of workflow nets from event logs. This algorithm was presented in the context of structured workflow nets even though it was recognized that more wokflow nets should be reconstructible. In this paper I assess \(\alpha\)-algorithm and provide a more precise description of the class of workflow nets reconstructible by \(\alpha\).