Timed Resource Driven Automata Nets for Distributed Real-Time Systems Modelling
The paper presents a formalism and a tool for modelling and analysis of distributed real-time systems of mobile agents. For that we use a time extension of our Resource Driven Automata Nets (TRDA-nets) formalism. A TRDA-net is a two-level system. The upper level represents distributed environment locations with a net of active resources. On the lower level agents are modeled by extended finite state machines, asynchronously consuming/producing shared resources through input/output system ports (arcs of the system net). We demonstrate modelling facilities of the formalism and show that specific layers of TRDA-nets can be translated into Timed Automata, as well as into Time Petri nets, thus TRDA-nets integrate merits of both formalisms.
Process mining is a relatively new field of computer science which deals with process discovery and analysis based on event logs. In this work we consider the problem of discovering workflow nets with cancellation regions from event logs. Cancellations occur in the majority of real-life event logs. In spite of huge amount of process mining techniques little has been done on cancellation regions discovery. We show that the state-based region algorithm gives labeled Petri nets with overcomplicated control flow structure for logs with cancellations. We propose a novel method to discover cancellation regions from the transition systems built on event logs and show the way to construct equivalent workflow net with reset arcs to simplify the control flow structure.
In this work we consider modeling of services with workflow modules, which are a subclass of Petri nets. The service compatibility problem is to answer the question, whether two Web services fit together, i.e. whether the composed system is sound. We study complementarity of service produced/consumed resources, that is a necessary condition for the service compatibility. Resources, which are produced/consumed by a Web service, are described as a multiset language. We define an algebra of multiset languages and present an algorithm for checking the conformance of resources for two given structured workflow modules.
This book constitutes the proceedings of the 37th International Conference on Application and Theory of Petri Nets and Concurrency, PETRI NETS 2016, held in Toruń, Poland, in June 2016. Petri Nets 2016 was co-located with the Application of Concurrency to System Design Conference, ACSD 2016. The 16 papers including 3 tool papers with 4 invited talks presented together in this volume were carefully reviewed and selected from 42 submissions. Papers presenting original research on application or theory of Petri nets, as well as contributions addressing topics relevant to the general field of distributed and concurrent systems are presented within this volume.
Process mining aims to discover and analyze processes by extracting information from event logs. Process mining discovery algorithms deal with large data sets to learn automatically process models. As more event data become available there is the desire to learn larger and more complex process models. To tackle problems related to the readability of the resulting model and to ensure tractability, various decomposition methods have been proposed. This paper presents a novel decomposition approach for discovering more readable models from event logs on the basis of a priori knowledge about the event log structure: regular and special cases of the process execution are treated separately. The transition system, corresponding to a given event log, is decomposed into a regular part and a specific part. Then one of the known discovery algorithms is applied to both parts, and finally these models are combined into a single process model. It is proven, that the structural and behavioral properties of submodels are inherited by the unified process model. The proposed discovery algorithm is illustrated using a running example.
These are the proceedings of the International Workshop on Petri Nets and Software Engineering (PNSE’13) and the International Workshop on Modeling and Business Environments (ModBE’13) in Milano, Italy, June 24–25, 2013. These are co-located events of Petri Nets 2013, the 34th international conference on Applications and Theory of Petri Nets and Concurrency.
PNSE'13 presents the use of Petri Nets (P/T-Nets, Coloured Petri Nets and extensions) in the formal process of software engineering, covering modelling, validation, and veriﬁcation, as well as their application and tools supporting the disciplines mentioned above.
ModBE’13 provides a forum for researchers from interested communities to investigate, experience, compare, contrast and discuss solutions for modeling in business environments with Petri nets and other modeling techniques.
Operational processes leave trails in the information systems supporting them. Such event data are the starting point for process mining – an emerging scientific discipline relating modeled and observed behavior. The relevance of process mining is increasing as more and more event data become available. The increasing volume of such data (“Big Data”) provides both opportunities and challenges for process mining. In this paper we focus on two particular types of process mining: process discovery (learning a process model from example behavior recorded in an event log) and conformance checking (diagnosing and quantifying discrepancies between observed behavior and modeled behavior). These tasks become challenging when there are hundreds or even thousands of different activities and millions of cases. Typically, process mining algorithms are linear in the number of cases and exponential in the number of different activities. This paper proposes a very general divide-and-conquer approach that decomposes the event log based on a partitioning of activities. Unlike existing approaches, this paper does not assume a particular process representation (e.g., Petri nets or BPMN) and allows for various decomposition strategies (e.g., SESE- or passage-based decomposition). Moreover, the generic divide-and-conquer approach reveals the core requirements for decomposing process discovery and conformance checking problems.
To verify realtime properties of UML statecharts one may apply a UPPAAL, toolbox for model checking of realtime systems. One of the most suitable ways to specify an operational semantics of UML statecharts is to invoke the formal model of Hierarchical Timed Automata. Since the model language of UPPAAL is based on Networks of Timed Automata one has to provide a conversion of Hierarchical Timed Automata to Networks of Timed Automata. In this paper we describe this conversion algorithm and prove that it is correct w.r.t. UPPAAL query language which is based on the subset of Timed CTL.