Search

This book offers a new Modular Petri Net as a solution to the vast Petri net models. It presents some approaches centering around modules (known as “Petri modules”). The goal of this book is to introduce a methodology in which Petri nets are moved to a new level. In this new level, large Petri net models are made of Petri modules, which are independent and run on different computers. This book also contains the literature study on modular Petri nets and definitions for the newer Petri modules. Also, algorithms for extracting Petri modules, and algorithms for connecting Petri modules, and applications are given in this book. Besides, the ideas and algorithms given in this book are implemented in the software General-purpose Petri Net Simulator (GPenSIM). Hence, with the use of this book the readers/users would be able to know that real-life discrete event systems could be modeled, analyzed, and performance-optimized with GPenSIM.

This book deals with the problem of finding suitable languages that can represent specific classes of Petri nets, the most studied and widely accepted model for distributed systems. Hence, the contribution of this book amounts to the alphabetization of some classes of distributed systems. The book also suggests the need for a generalization of Turing computability theory.It is important for graduate students and researchers engaged with the concurrent semantics of distributed communicating systems. The author assumes some prior knowledge of formal languages and theoretical computer science.

Petri nets are a formal and theoretically rich model for the modelling and analysis of systems. A subclass of Petri nets, augmented marked graphs possess a structure that is especially desirable for the modelling and analysis of systems with concurrent processes and shared resources.This monograph consists of three parts: Part I provides the conceptual background for readers who have no prior knowledge on Petri nets; Part II elaborates the theory of augmented marked graphs; finally, Part III discusses the application to system integration. The book is suitable as a first self-contained volume on augmented marked graphs, and will be useful to both researchers and practitioners in the fields of Petri nets and system integration.

This book presents a coherent description of the theoretical and practical aspects of Coloured Petri Nets (CP-nets or CPN). It shows how CP-nets have been de­ veloped - from being a promising theoretical model to being a full-fledged lan­ guage for the design, specification, simulation, validation and implementation of large software systems (and other systems in which human beings and/or com­ puters communicate by means of some more or less formal rules). The book contains the formal definition of CP-nets and the mathematical theory behind their analysis methods. However, it has been the intention to write the book in such a way that it also becomes attractive to readers who are more interested in applications than the underlying mathematics. This means that a large part of the book is written in a style which is closer to an engineering textbook (or a users'manual) than it is to a typical textbook in theoretical computer science. The book consists of three separate volumes. The first volume defines the net model (i. e., hierarchical CP-nets) and the basic concepts (e. g., the different behavioural properties such as deadlocks, fair­ ness and home markings). It gives a detailed presentation of many small exam­ ples and a brief overview of some industrial applications. It introduces the for­ mal analysis methods. Finally, it contains a description of a set of CPN tools which support the practical use of CP-nets.

This book presents a coherent description of the theoretical and practical aspects of Coloured Petri Nets (CP-nets or CPN). It shows how CP-nets have been de­ veloped - from being a promising theoretical model to being a full-fledged lan­ guage for the design, specification, simulation, validation and implementation of large software systems (and other systems in which human beings and/or com­ puters communicate by means of some more or less formal rules). The book contains the formal definition of CP-nets and the mathematical theory behind their analysis methods. However, it has been the intention to write the book in such a way that it also becomes attractive to readers who are more interested in applications than the underlying mathematics. This means that a large part of the book is written in a style which is closer to an engineering textbook (or a users'manual) than it is to a typical textbook in theoretical computer science. The book consists of three separate volumes. The first volume defines the net model (i. e., hierarchical CP-nets) and the basic concepts (e. g., the different behavioural properties such as deadlocks, fair­ ness and home markings). It gives a detailed presentation of many smaIl exam­ ples and a brief overview of some industrial applications. It introduces the for­ mal analysis methods. FinaIly, it contains a description of a set of CPN tools which support the practical use of CP-nets.

With their intuitive graphical approach and expressive analysis techniques, Petri nets are suitable for a wide range of applications and teaching scenarios, and they have gained wide acceptance as a modeling technique in areas such as software design and control engineering. The core theoretical principles have been studied for many decades and there is now a comprehensive research literature that complements the extensive implementation experience.In this book the author presents a clear, thorough introduction to the essentials of Petri nets. He explains the core modeling techniques and analysis methods and he illustrates their usefulness with examples and case studies. Part I describes how to use Petri nets for modeling; all concepts are explained with the help of examples, starting with a generic, powerful model which is also intuitive and realistic. Part II covers the essential analysis methods that are specific to Petri nets, introducing techniques used to formulate keyproperties of system nets and algorithms for proving their validity. Part III presents case studies, each introducing new concepts, properties and analysis techniques required for very different modeling tasks. The author offers different paths among the chapters and sections: the elementary strand for readers who wish to study only elementary nets; the modeling strand for those who wish to study the modeling but not the analysis of systems; and finally the elementary models of the modeling strand for those interested in technically simple, but challenging examples and case studies.The author achieves an excellent balance between consistency, comprehensibility and correctness in a book of distinctive design. Among its characteristics, formal arguments are reduced to a minimum in the main text with many of the theoretical formalisms moved to an appendix, the explanations are supported throughout with fully integrated graphical illustrations, and each chapter ends with exercises and recommendations for further reading.The book is suitable for students of computer science and related subjects such as engineering, and for a broad range of researchers and practitioners.

High-level Petri nets are now widely used in both theoretical analysis and practical modelling of concurrent systems. The main reason for the success of this class of net models is that they make it possible to obtain much more succinct and manageable de­ scriptions than can be obtained by means of low-level Petri nets-while, on the other hand, they still offer a wide range of analysis methods and tools. The step from low-level nets to high-level nets can be compared to the step from assembly languages to modem programming languages with an elaborated type concept. In low-level nets there is only one kind of token and this means that the state of a place is described by an integer (and in many cases even by a boolean value). In high-level nets each token can carry complex information which, e. g., may describe the entire state of a process or a data base. Today most practical applications of Petri nets use one of the different kinds of high-level nets. A considerable body of knowledge exists about high-level Petri nets­ this includes theoretical foundations, analysis methods and many applications. Unfortunately, the papers on high-level Petri nets have been scattered throughout various journals and collections. As a result, much of this knowledge is not readily available to people who may be interested in using high-level nets.

Petri nets provide a formal framework for system modeling and validation which has proven to be very reliable in practice. This book presents variousnet models appropriate for designing specific systems, where systems are understood very generally as'organizational systems'in which regulatedflows of objects and information are significant. The models are interrelated in the sense that they have common interpretation patterns: together they can be understood as a method for specifying any given system or any section of such a system to any given degree of refinement. The simple and immediately understandable principles of system modelling with nets makes it possible to provide an illustrated description of this method without going into the mathematics behind it. The text is based on courses the author developed for project engineers and project managers in the area of embedded computer systems.

In a component-based approach for system design, one of the challenging problems is the way to prove the correctness of the created components. Usually, the constituent components are supposed to be correct — possessing the desirable properties and free from undesirable ones. However, the operators may destroy these properties or create new ones, resulting in an undesirable new component. Hence, every created component has to go through a new process of verification, involving a tremendous amount of effort.This book presents a component -based methodology for the creation and verification of design specifications. The methodology is formally presented as an algebra called Property-Preserving Petri Net Process Algebra (PPPA). PPPA includes five classes of operators, and the authors show that every operator of PPPA can preserve a large number of basic system properties. Therefore, if the initial set of primitive components satisfies some of these properties, the created components will also “automatically” satisfy them without the need for further verification — thus greatly saving verification efforts.

Coloured Petri Nets (CPN) is a graphical language for modelling and validating concurrent and distributed systems, and other systems in which concurrency plays a major role. The development of such systems is particularly challenging because of inherent intricacies like possible nondeterminism and the immense number of possible execution sequences. In this textbook Jensen and Kristensen introduce the constructs of the CPN modelling language and present the related analysis methods in detail. They also provide a comprehensive road map for the practical use of CPN by showcasing selected industrial case studies that illustrate the practical use of CPN modelling and validation for design, specification, simulation, verification and implementation in various application domains. Their presentation primarily aims at readers interested in the practical use of CPN. Thus all concepts and constructs are first informally introduced through examples and then followed by formal definitions (which may be skipped). The book is ideally suitable for a one-semester course at an advanced undergraduate or graduate level, and through its strong application examples can also serve for self-study. An accompanying website offers additional material such as slides, exercises and project proposals. Book website: http://www.cs.au.dk/CPnets/cpnbook/

Deadlock problems in flexible manufacturing systems (FMS) have received more and more attention in the last two decades. Petri nets are one of the more promising mathematical tools for tackling deadlocks in various resource allocation systems. In a system modeled with Petri nets, siphons are tied to the occurrence of deadlock states as a structural object. The book systematically introduces the novel theory of siphons, traps, and elementary siphons of Petri nets as well as the deadlock control strategies for FMS developed from it. Deadlock prevention methods are examined comparatively. The many FMS examples presented to demonstrate the concepts and results of this book range from the simple to the complex. Importantly, to inspire and motive the reader's interest in further research, a number of interesting and open problems in this area are proposed at the end of each chapter.

Foundation of logic historically dates back to the times of Aristotle, who pioneered the concept of truth/falsehood paradigm in reasoning. Mathematical logic of propositions and predicates, which are based on the classical models of Aristotle, underwent a dramatic evolution during the last 50 years for its increasing applications in automated reasoning on digital computers. The subject of Logic Programming is concerned with automated reasoning with facts and knowledge to answer a user's query following the syntax and semantics of the logic of propositions/predicates. The credit of automated reasoning by logic programs goes to Professor Robinson for his well-known resolution theorem that provides a general scheme to select two program clauses for deriving an inference. Until now Robinson's theorem is being used in PROLOG/DATALOG compilers to automatically build a Select Linear Definite (SLD) clause based resolution tree for answering a user's query. The SLD-tree based scheme for reasoning undoubtedly opened a new era in logic programming for its simplicity in implementation in the compilers. In fact, SLD-tree construction suffices the need for users with a limited set of program clauses. But with increase in the number of program clauses, the execution time of the program also increases linearly by the SLD-tree based approach. An inspection of a large number of logic programs, however, reveals that more than one pair of program clauses can be resolved simultaneously without violating the syntax and the semantics of logic programming. This book employs this principle to speed up the execution time of logic programs.

Formal methods for the specification and verification of hardware and software systems are becoming more and more important as systems increase in size and complexity. The aim of the book is to illustrate progress in formal methods, based on Petri net formalisms. It contains a collection of examples arising from different fields, such as flexible manufacturing, telecommunication and workflow management systems.The book covers the main phases in the life cycle of design and implementation of a system, i.e., specification, model checking techniques for verification, analysis of properties, code generation, and execution of models. These techniques and their tool support are discussed in detail including practical issues. Amongst others, fundamental concepts such as composition, abstraction, and reusability of models, model verification, and verification of properties are systematically introduced.