Petri nets behavioral equivalence checking in SMV
This paper proposes an approach to k-bounded Petri nets behavioral equivalence checking using the model checking method and mainstream verifier nuSMV. For the comparison of behavior of two nets, an add-in net is introduced which performs a supervisory control of these two nets. The approach uses an implicit word-to-word comparison of labeled Petri net languages with invisible transitions when computing CTL temporal logic formulas. The technique of Petri nets equivalence checking in SMV is briefly discussed followed by a simple case study.
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.
Despite all the advantages brought by service-oriented architecture (SOA), experts argue that SOA introduces more complexity into information systems rather than resolving it. The problem of service integration challenges modern companies taking the risk of implementing SOA. One of important aspects of this problem relates to dynamic service composition, which has to take into account many types of information and restrictions existing in each enterprise. Moreover, all the changes in business logic should also be promptly reflected. This chapter proposes the approach to solution of the stated problem based on such concepts as model-driven architecture (MDA), ontology modelling and logical analysis. The approach consists of several steps of modelling and finite scope logical analysis for automated translation of business processes into the sequence of service invocations. Formal language of relational logic is proposed as a key element of the proposed approach which is responsible for logical analysis and service workflow generation. We present a logical theory to automatically specialize generic orchestration templates which are close to semantic specification of abstract services in OWL-S. The developed logical theory is described formally in terms of Relational Logic. Our approach is implemented and tested using MIT Alloy Analyzer software.
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.
Resource-driven automata (RDA) are finite automata, sitting in the nodes of a finite system net and asynchronously consuming/producing shared resources through input/output system ports (arcs of the system net). RDAs themselves may be resources for each other, thus allowing the highly flexible structure of the model. It was proved earlier, that RDA-nets are expressively equivalent to Petri nets. In this paper the new formalism of cellular RDAs is introduced. Cellular RDAs are RDA-nets with an infinite regularly structured system net. We build a hierarchy of cellular RDA classes on the basis of restrictions on the underlying grid. The expressive power of several major classes of 1-dimensional grids is studied.
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.
This volume constitutes the refereed proceedings of the 37th International Symposium on Mathematical Foundations of Computer Science, MFCS 2012, held in Bratislava, Slovakia, in August 2012. The 63 revised full papers presented together with 8 invited talks were carefully reviewed and selected from 162 submissions. Topics covered include algorithmic game theory, algorithmic learning theory, algorithms and data structures, automata, formal languages, bioinformatics, complexity, computational geometry, computer-assisted reasoning, concurrency theory, databases and knowledge-based systems, foundations of computing, logic in computer science, models of computation, semantics and verification of programs, and theoretical issues in artificial intelligence.