Ponències/Comunicacions de congressos
http://hdl.handle.net/2117/3095
2017-02-22T13:12:05ZMining structured Petri nets for the visualization of process behavior
http://hdl.handle.net/2117/100797
Mining structured Petri nets for the visualization of process behavior
San Pedro Martín, Javier de; Cortadella Fortuny, Jordi
Visualization is essential for understanding the models obtained by process mining. Clear and efficient visual representations make the embedded information more accessible and analyzable. This work presents a novel approach for generating process models with structural properties that induce visually friendly layouts. Rather than generating a single model that captures all behaviors, a set of Petri net models is delivered, each one covering a subset of traces of the log. The models are mined by extracting slices of labelled transition systems with specific properties from the complete state space produced by the process logs. In most cases, few Petri nets are sufficient to cover a significant part of the behavior produced by the log.
2017-02-10T08:35:24ZSan Pedro Martín, Javier deCortadella Fortuny, JordiVisualization is essential for understanding the models obtained by process mining. Clear and efficient visual representations make the embedded information more accessible and analyzable. This work presents a novel approach for generating process models with structural properties that induce visually friendly layouts. Rather than generating a single model that captures all behaviors, a set of Petri net models is delivered, each one covering a subset of traces of the log. The models are mined by extracting slices of labelled transition systems with specific properties from the complete state space produced by the process logs. In most cases, few Petri nets are sufficient to cover a significant part of the behavior produced by the log.Comparing MapReduce and pipeline implementations for counting triangles
http://hdl.handle.net/2117/100579
Comparing MapReduce and pipeline implementations for counting triangles
Pasarella Sánchez, Ana Edelmira; Vidal Serodio, Maria Esther; Zoltan, Cristina
A generalized method to define the Divide & Conquer paradigm in order to have processors acting on its own data and scheduled in a
parallel fashion. MapReduce is a programming model that follows this paradigm, and allows for the definition of efficient solutions by both decomposing a problem into steps on subsets of the input data
and combining the results of each step to produce final results. Albeit used for the implementation of a wide variety of computational problems, MapReduce performance can be negatively affected
whenever the replication factor grows or the size of the input is larger than the resources available at each processor. In this paper we show an alternative approach to implement the Divide & Conquer
paradigm, named pipeline. The main features of pipeline are illustrated on a parallel implementation of the well-known problem of counting triangles in a graph. This problem is especially interesting either when the input graph does not fit in memory or is dynamically generated. To evaluate the properties of pipeline, a dynamic pipeline of processes and an ad-hoc version of MapReduce are implemented in the language Go, exploiting its ability to deal with channels and spawned processes.
An empirical evaluation is conducted on graphs of different sizes and densities. Observed results suggest that pipeline allows for the implementation of an efficient solution of the problem of counting
triangles in a graph, particularly, in dense and large graphs, drastically reducing the execution time with respect to the MapReduce implementation.
2017-02-06T08:48:11ZPasarella Sánchez, Ana EdelmiraVidal Serodio, Maria EstherZoltan, CristinaA generalized method to define the Divide & Conquer paradigm in order to have processors acting on its own data and scheduled in a
parallel fashion. MapReduce is a programming model that follows this paradigm, and allows for the definition of efficient solutions by both decomposing a problem into steps on subsets of the input data
and combining the results of each step to produce final results. Albeit used for the implementation of a wide variety of computational problems, MapReduce performance can be negatively affected
whenever the replication factor grows or the size of the input is larger than the resources available at each processor. In this paper we show an alternative approach to implement the Divide & Conquer
paradigm, named pipeline. The main features of pipeline are illustrated on a parallel implementation of the well-known problem of counting triangles in a graph. This problem is especially interesting either when the input graph does not fit in memory or is dynamically generated. To evaluate the properties of pipeline, a dynamic pipeline of processes and an ad-hoc version of MapReduce are implemented in the language Go, exploiting its ability to deal with channels and spawned processes.
An empirical evaluation is conducted on graphs of different sizes and densities. Observed results suggest that pipeline allows for the implementation of an efficient solution of the problem of counting
triangles in a graph, particularly, in dense and large graphs, drastically reducing the execution time with respect to the MapReduce implementation.A semantics of business configurations using symbolic graphs
http://hdl.handle.net/2117/100385
A semantics of business configurations using symbolic graphs
Mylonakis Pascual, Nicolás; Orejas Valdés, Fernando; Fiadeiro, José Luiz
In this paper we give graph-semantics to a fundamental part of the semantics of the service modeling language SRML: business configurations. To achieve this goal we use symbolic graph transformation systems. We formalize the semantics using this graph transformation system and illustrating it with a simple running example of a trip booking agent.
2017-01-31T13:43:47ZMylonakis Pascual, NicolásOrejas Valdés, FernandoFiadeiro, José LuizIn this paper we give graph-semantics to a fundamental part of the semantics of the service modeling language SRML: business configurations. To achieve this goal we use symbolic graph transformation systems. We formalize the semantics using this graph transformation system and illustrating it with a simple running example of a trip booking agent.Conditions for compatibility of components: The case of masters and slaves
http://hdl.handle.net/2117/100199
Conditions for compatibility of components: The case of masters and slaves
Beek, Maurice ter; Carmona Vargas, Josep; Kleijn, Jetty
We consider systems composed of reactive components that collaborate through synchronised execution of common actions. These multi-component systems are formally represented as team automata, a model that allows a wide spectrum of synchronisation policies to combine components into higher-level systems. We investigate the
correct-by-construction engineering of such systems of systems from the point of view of correct communications between the components (no message loss or deadlocks due to indefinite waiting). This leads to a proposal for a generic definition of compatibility of components relative to the adopted synchronisation policy. This definition appears
to be particularly appropriate for so-called master-slave synchronisations by which input actions (for `slaves') are driven
by output actions (from `masters').
2017-01-27T12:09:50ZBeek, Maurice terCarmona Vargas, JosepKleijn, JettyWe consider systems composed of reactive components that collaborate through synchronised execution of common actions. These multi-component systems are formally represented as team automata, a model that allows a wide spectrum of synchronisation policies to combine components into higher-level systems. We investigate the
correct-by-construction engineering of such systems of systems from the point of view of correct communications between the components (no message loss or deadlocks due to indefinite waiting). This leads to a proposal for a generic definition of compatibility of components relative to the adopted synchronisation policy. This definition appears
to be particularly appropriate for so-called master-slave synchronisations by which input actions (for `slaves') are driven
by output actions (from `masters').Non-homogenizable classes of finite structures
http://hdl.handle.net/2117/100189
Non-homogenizable classes of finite structures
Atserias, Albert; Torunczyk, Szymon Abram
Homogenization is a powerful way of taming a class of finite structures with several interesting applications in different areas, from Ramsey theory in combinatorics to constraint satisfaction problems (CSPs) in computer science, through (finite) model theory. A few sufficient conditions for a class of finite structures to allow homogenization are known, and here we provide a necessary condition. This lets us show that certain natural classes are not homogenizable: 1) the class of locally consistent systems of linear equations over the two-element field or any finite Abelian group, and 2) the class of finite structures that forbid homomorphisms from a specific MSO-definable class of structures of treewidth two. In combination with known results, the first example shows that, up to pp-interpretability, the CSPs that are solvable by local consistency methods are distinguished from the rest by the fact that their classes of locally consistent instances are homogenizable. The second example shows that, for MSO-definable classes of forbidden patterns, treewidth one versus two is the dividing line to homogenizability.
2017-01-27T10:51:13ZAtserias, AlbertTorunczyk, Szymon AbramHomogenization is a powerful way of taming a class of finite structures with several interesting applications in different areas, from Ramsey theory in combinatorics to constraint satisfaction problems (CSPs) in computer science, through (finite) model theory. A few sufficient conditions for a class of finite structures to allow homogenization are known, and here we provide a necessary condition. This lets us show that certain natural classes are not homogenizable: 1) the class of locally consistent systems of linear equations over the two-element field or any finite Abelian group, and 2) the class of finite structures that forbid homomorphisms from a specific MSO-definable class of structures of treewidth two. In combination with known results, the first example shows that, up to pp-interpretability, the CSPs that are solvable by local consistency methods are distinguished from the rest by the fact that their classes of locally consistent instances are homogenizable. The second example shows that, for MSO-definable classes of forbidden patterns, treewidth one versus two is the dividing line to homogenizability.A logic of graph conditions extended with paths
http://hdl.handle.net/2117/100161
A logic of graph conditions extended with paths
Navarro Gomez, Marisa; Orejas Valdés, Fernando; Pino Blanco, Elvira; Lambers, Leen
In this paper we tackle the problem of extending the logic of nested graph conditions with paths. This means, for instance, that we may state properties about the existence of paths between some given nodes. As a main contribution, a sound and complete tableau method is defined for reasoning about this kind of properties.
2017-01-27T09:01:41ZNavarro Gomez, MarisaOrejas Valdés, FernandoPino Blanco, ElviraLambers, LeenIn this paper we tackle the problem of extending the logic of nested graph conditions with paths. This means, for instance, that we may state properties about the existence of paths between some given nodes. As a main contribution, a sound and complete tableau method is defined for reasoning about this kind of properties.A logic of graph conditions extended with paths
http://hdl.handle.net/2117/100160
A logic of graph conditions extended with paths
Navarro Gomez, Marisa; Orejas Valdés, Fernando; Pino Blanco, Elvira; Lambers, Leen
In this paper we tackle the problem of extending the logic of nested graph conditions with paths. This means, for instance, that we may state properties about the existence of paths between some given nodes. As a main contribution, a sound and complete tableau method is defined for reasoning about this kind of properties.
2017-01-27T08:56:31ZNavarro Gomez, MarisaOrejas Valdés, FernandoPino Blanco, ElviraLambers, LeenIn this paper we tackle the problem of extending the logic of nested graph conditions with paths. This means, for instance, that we may state properties about the existence of paths between some given nodes. As a main contribution, a sound and complete tableau method is defined for reasoning about this kind of properties.Specification mining for asynchronous controllers
http://hdl.handle.net/2117/99949
Specification mining for asynchronous controllers
San Pedro Martín, Javier de; Bourgeat, Thomas; Cortadella Fortuny, Jordi
The paper presents a first effort at exploring a novel area in the domain of asynchronous controllers: specification mining. Rather than synthesizing circuits from specifications, we aim at doing reverse engineering, i.e., discovering safe specifications from the circuits that preserve a set of pre-defined behavioral properties (e.g., hazard freeness). The specifications are discovered without any previous knowledge of the behavior of the circuit environment.
This area may open new opportunities for re-synthesis and verification of asynchronous controllers. The effectiveness of the proposed approach is demonstrated by mining concurrent specifications (Signal Transition Graphs) from multiple implementations of 4-phase handshake controllers and some controllers with choice.
2017-01-24T13:19:10ZSan Pedro Martín, Javier deBourgeat, ThomasCortadella Fortuny, JordiThe paper presents a first effort at exploring a novel area in the domain of asynchronous controllers: specification mining. Rather than synthesizing circuits from specifications, we aim at doing reverse engineering, i.e., discovering safe specifications from the circuits that preserve a set of pre-defined behavioral properties (e.g., hazard freeness). The specifications are discovered without any previous knowledge of the behavior of the circuit environment.
This area may open new opportunities for re-synthesis and verification of asynchronous controllers. The effectiveness of the proposed approach is demonstrated by mining concurrent specifications (Signal Transition Graphs) from multiple implementations of 4-phase handshake controllers and some controllers with choice.A recursive paradigm for aligning observed behavior of large structured process models
http://hdl.handle.net/2117/99940
A recursive paradigm for aligning observed behavior of large structured process models
Taymouri, Farbod; Carmona Vargas, Josep
The alignment of observed and modeled behavior is a crucial problem in process mining, since it opens the door for conformance checking and enhancement of process models. The state of the art techniques for the computation of alignments rely on a full exploration of the combination of the model state space and the observed behavior (an event log), which hampers their applicability for large instances. This paper presents a fresh view to the alignment problem: the computation of alignments is casted as the resolution of Integer Linear Programming models, where the user can decide the granularity of the alignment steps. Moreover, a novel recursive strategy is used to split
the problem into small pieces, exponentially reducing the complexity of the ILP models to be solved. The contributions of this paper represent a promising alternative to fight the inherent complexity of computing alignments for large instances.
2017-01-24T12:28:52ZTaymouri, FarbodCarmona Vargas, JosepThe alignment of observed and modeled behavior is a crucial problem in process mining, since it opens the door for conformance checking and enhancement of process models. The state of the art techniques for the computation of alignments rely on a full exploration of the combination of the model state space and the observed behavior (an event log), which hampers their applicability for large instances. This paper presents a fresh view to the alignment problem: the computation of alignments is casted as the resolution of Integer Linear Programming models, where the user can decide the granularity of the alignment steps. Moreover, a novel recursive strategy is used to split
the problem into small pieces, exponentially reducing the complexity of the ILP models to be solved. The contributions of this paper represent a promising alternative to fight the inherent complexity of computing alignments for large instances.A unified approach for measuring precision and generalization based on anti-alignments
http://hdl.handle.net/2117/99938
A unified approach for measuring precision and generalization based on anti-alignments
Dongen, Boudewijn van; Carmona Vargas, Josep; Chatain, Thomas
The holy grail in process mining is an algorithm that, given an event log, produces fitting, precise, properly generalizing and simple process models. While there is consensus on the existence of solid metrics for fitness and simplicity, current metrics for precision and generalization have important flaws, which hamper their applicability in a general setting. In this paper, a novel approach to measure precision and generalization is presented, which relies on the notion of antialignments. An anti-alignment describes highly deviating model traces with respect to observed behavior. We propose metrics for precision and generalization that resemble the leave-one-out cross-validation techniques, where individual traces of the log are removed and the computed anti-alignment assess the model’s capability to describe precisely or generalize the observed behavior. The metrics have been implemented in ProM and tested on several examples.
2017-01-24T12:12:26ZDongen, Boudewijn vanCarmona Vargas, JosepChatain, ThomasThe holy grail in process mining is an algorithm that, given an event log, produces fitting, precise, properly generalizing and simple process models. While there is consensus on the existence of solid metrics for fitness and simplicity, current metrics for precision and generalization have important flaws, which hamper their applicability in a general setting. In this paper, a novel approach to measure precision and generalization is presented, which relies on the notion of antialignments. An anti-alignment describes highly deviating model traces with respect to observed behavior. We propose metrics for precision and generalization that resemble the leave-one-out cross-validation techniques, where individual traces of the log are removed and the computed anti-alignment assess the model’s capability to describe precisely or generalize the observed behavior. The metrics have been implemented in ProM and tested on several examples.