Wyniki wyszukiwania - BazTech

1

Incremental Process Discovery using Petri Net Synthesis

Badouel E., Schlachter U.

Fundamenta Informaticae

|

2017

|

Vol. 154, nr 1/4

1--13

EN

Process discovery aims at constructing a model from a set of observations given by execution traces (a log). Petri nets are a preferred target model in that they produce a compact description of the system by exhibiting its concurrency. This article presents a process discovery algorithm using Petri net synthesis, based on the notion of region introduced by A. Ehrenfeucht and G. Rozenberg and using techniques from linear algebra. The algorithm proceeds in three successive phases which make it possible to find a compromise between the ability to infer behaviours of the system from the set of observations while ensuring a parsimonious model, in terms of fitness, precision and simplicity. All used algorithms are incremental which means that one can modify the produced model when new observations are reported without reconstructing the model from scratch.

2

Petri Nets with Structured Data

Badouel E., Hélouët L., Morvan C.

Fundamenta Informaticae

|

2016

|

Vol. 146, nr 1

35--82

EN

This paper considers Structured Data Nets (StDN): a Petri net extension that describes open systems with data. The objective of this language is to serve as a formal basis for the analysis of systems that use data, accept inputs from their environment, and implement complex workflows. In StDNs, tokens are structured documents. Each transition is attached to a query, guarded by patterns, (logical assertions on the contents of its preset) and transforms tokens. We define StDNs and their semantics. We then consider their formal properties: coverability of a marking, termination and soundness of transactions. Unrestricted StDNs are Turing complete, so coverability, termination and soundness are undecidable for StDNs. However, using an order on documents, and putting reasonable restrictions both on the expressiveness of patterns and queries and on the documents, we show that StDNs are well-structured transition systems, for which coverability, termination and soundness are decidable. We then show the expressive power of StDN on a case study, and compare StDNs and their decidable subclasses with other types of high-level nets and other formalisms adapted to data-centric approaches or to workflows design.

3

A Modal Interface Theory for Component-based Design

Raclet J. B., Benveniste A., Legay A., Badouel E., Caillaud B., Passerone R.

Fundamenta Informaticae

|

2011

|

Vol. 108, nr 1/2

119-149

EN

This paper presents the modal interface theory, a unification of interface automata and modal specifications, two radically dissimilar models for interface theories. Interface automata is a game-basedmodel, 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. The work reported here is based on earlier work presented in [41] and [42].

4

An Axiomatization of the Token Game Based on Petri Algebras

Badouel E., Chenou J., Guillou G.

Fundamenta Informaticae

|

2007

|

Vol. 77, nr 3

187-215

EN

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.