The Infona portal uses cookies, i.e. strings of text saved by a browser on the user's device. The portal can access those files and use them to remember the user's data, such as their chosen settings (screen view, interface language, etc.), or their login data. By using the Infona portal the user accepts automatic saving and using this information for portal operation purposes. More information on the subject can be found in the Privacy Policy and Terms of Service. By closing this window the user confirms that they have read the information on cookie usage, and they accept the privacy policy and the way cookies are used by the portal. You can change the cookie settings in your browser.
Literature on the stubborn set and similar state space reduction methods presents numerous seemingly ad-hoc conditions for selecting the transitions that are investigated in the current state. There are good reasons to believe that the choice between them has a significant effect on reduction results, but not much has been published on this topic. This article presents theoretical results and examples...
Identification of behavioural contradictions is an important aspect of software engineering, in particular for checking the consistency between a business process model used as system specification and a corresponding workflow model used as implementation. In this paper, we propose causal behavioural profiles as the basis for a consistency notion, which capture essential behavioural information, such...
A new partial order semantics called canonical transition set (CTS for short) semantics is proposed for P/T nets. We first prove that it is well-defined, sound and complete, and then give a state space exploring method based on it. CTS semantics provides a compressed representation for the interleaving transition sequences of finite length. Compared with other methods, the state space exploration...
This paper defines a class of labeled stratified order structures that characterizes exactly the notion of combined traces (i.e., comtraces) proposed by Janicki and Koutny in 1995. Our main technical contributions are the representation theorems showing that comtrace quotient monoid, combined dependency graph (Kleijn and Koutny 2008) and our labeled stratified order structure characterization are...
We present a methodology for integrated process planning and supply chain configuration for commodity assemblies. Although the supply chain configuration problem for commodity assemblies is relatively straightforward using math programming, developing a commodity-dependent math program with precedence constraints can be a very daunting and time-consuming process. We use Petri net techniques to support...
This paper presents the modelling process and first analysis results carried out within the NEOPPOD project. A protocol, NEO, has been designed in order to manage very large distributed databases such as those used for banking and e-government applications, and thus to handle sensitive data. Security of data is therefore a critical issue that must be ensured before the software can be released on...
The unfolding technique is an efficient tool to explore the runs of a Petri net in a true concurrency semantics, i.e. without constructing all the interleavings of concurrent actions. But even small real systems are never modeled directly as ordinary Petri nets: they use many high-level features that were designed as extensions of Petri nets. We focus here on two such features: colors and compositionality...
Pure names are identifiers with no relation between them, except equality and inequality. In previous works we have extended P/T nets with the capability of creating and managing pure names, obtaining ν-APNs and proved that they are strictly well structured (WSTS), so that coverability and boundedness are decidable. Here we use the framework recently developed by Finkel and Goubault-Larrecq for forward...
Workflow mining is the task of automatically producing a workflow model from a set of event logs recording sequences of workflow events; each sequence corresponds to a use case or workflow instance. Formal approaches to workflow mining assume that the event log is complete (contains enough information to infer the workflow) which is often not the case. We present a learning approach that relaxes this...
A central problem in the area of Process Mining is to obtain a formal model that represents selected behavior of a system. The theory of regions has been applied to address this problem, enabling the derivation of a Petri net whose language includes a set of traces. However, when dealing with real-life systems, the available tool support for performing such task is unsatisfactory, due to the complex...
The siphon-trap property, also known as Commoner-Hack property, establishes a relation between structural entities within a Petri net – the eponymous siphons and traps. The property is linked to the behavior of a Petri net, for instance to deadlock freedom and liveness of the net. It is nevertheless nontrivial to decide the property as a net can have exponentially many siphons and traps even if only...
In the paper we discuss the event-driven reactive programs and systems, which does not deadlock for one instance, but because of shared resources, can deadlock for several instances. We focus on event-driven programs, where instances have a correct finish, and resources can be used by single instances, but can neither be destroyed nor created by instances. Typical examples include workflow processes,...
This talk starts from a dream/vision paper I published in 2008, whose title is a play on that of John Backus’ famous Turing Award Lecture (and paper); see [3]. I will propose that — or rather ask whether — programming can be made to be a lot closer to the way humans think about dynamics, and the way they manage to get others (e.g., their children, their employees, etc.) to do what they have in mind...
In this survey paper, we discuss how to enhance the modelling power of Place/Transition-nets with the notions of ‘locality’ of individual transitions and token ‘testing’ using inhibitor and activator arcs (or, more generally, range arcs). As motivation for these extensions we consider membrane systems – a computational model inspired by the way chemical reactions take place in cells that are divided...
We provide a chronological research perspective on the development and application of methods and supporting computer tools for state space exploration and model checking of Coloured Petri Nets. We discuss how the lessons learned from practical applications have influenced current and envisioned future research directions concentrating on the ongoing development of the ASAP state space exploration...
AlPiNA is a symbolic model checker for High Level Petri nets. It is comprised of two independent modules: a GUI plugin for Eclipse and an underlying model checking engine. AlPiNA’s objective is to perform efficient and user-friendly, easy to use model checking of large software systems. This is achieved by separating the model and its properties from the model checking-related concerns: the users...
Service-oriented computing proposes services as building blocks which can be composed to complex systems. To reason about the correctness of a service, its communication protocol needs to be analyzed. A fundamental correctness criterion for a service is the existence of a partner service, formalized in the notion of controllability. In this paper, we introduce Wendy, a Petri net-based tool...
Decision diagrams (DDs) have made their way into Petri net (PN) tools either in the form of new tools (usually designed from scratch to use DDs) or as enhancements to existing tools. This paper describes how an existing and established tool (GreatSPN) has been enhanced through the use of DDs provided by an existing open-source library (Meddly). We benchmark the enhanced tool and discuss lessons learned...
The International Standard on Petri nets, ISO/IEC 15909, provides a formal semantics and syntax to enable model interchange and industrial dissemination. Part 2 defines a concrete interchange format as an XML-based language: PNML. This language is bound to evolve together with future developments of the standard. This paper presents PNML Framework, a companion implementation of the standard...
Set the date range to filter the displayed results. You can set a starting date, ending date or both. You can enter the dates manually or choose them from the calendar.