 | This article may be too technical for most readers to understand.(April 2019) |
Nets within Nets is a modelling method belonging to the family of Petri nets. This method is distinguished from other sorts of Petri nets by the possibility to provide their tokens with a proper structure, which is based on Petri net modelling again. Hence, a net can contain further net items, being able to move around and fire themselves.
Nets within nets are well suited for the modelling of distributed systems under the particular aspects of
In a lot of publications in relation to object-oriented design is given, in order to combine the ability of Petri nets in modelling distributed computing with the modelling of objects, being able to be created and to interact.
Starting from the need of practical applications, by the mid of nineties, different formalisms have been created, which fit the description of „nets within nets“. Lomazova and Schnoebelen are listing [1] some of these approaches, namely by Sibertin-Blanc, [2] Lakos, [3] Moldt und Wienberg [4] as extending Coloured Petri nets, aside the Object Nets of Valk. [5] The earliest use of such hierarchic net models appeared by Rüdiger Valk in Valk and Jessen, [6] where the so-called task-flow nets [7] are introduced in order to model task systems in operating systems. In these models tasks are modelled by a Petri net, which represents the precedences of tasks and their state of execution.
The most important differences in semantics is given by the execution of net tokens. On the one side net tokens can be references to net items, [8] which case is called „reference semantics“. This kind of semantic is distinguished from value semantics, where net objects may exist in different places and different internal states. In value semantics different copies can be created to model concurrent execution. The corresponding join of such a split can be defined in different ways, as for instance by „distributed token semantics“ [9] or „history process semantics“. [10] In connection with mobile computing hybrid versions of reference and value semantics are of importance. [11] In distributed token semantics the important calculus of place invariants for Petri nets remains valid. [12]
The formalism of nets within nets would be of few importance without communication between net tokens. Like in object-oriented programming communication of net tokens is introduced via predefined interfaces which are dynamically bound.
In Figure 1 a Petri net is shown containing a token Petri net in place „a“. The token net can move around from place „a“ to place „b“ and back by firing of the transitions of the outer net. The channel inscriptions at the transitions behave like a call of a method, resulting in the synchronised firing of the calling transition in the outer net [e.g. labelled by x:forth()] and the called transition [e.g. labelled by :forth()] in the token net. The variable „x“ at an arrow is bound to the token net in the place connected with this arrow. The brackets may contain parameters to be passed. This example is so simple that reference and value semantics coincide.
Standard Petri net properties like reachability, boundedness and liveness show a mixed picture. A paper [13] of Köhler-Bußmeier gives a survey on decidability results for elementary object systems. To reduce the complexity of the formalism subclasses have been defined by restricting the structure of the Petri nets, as for instance to state machines. Such restrictions still allow complex modelling of distributed and mobile systems, but have polynomial complexity in model checking. [14]
In computer science, formal methods are mathematically rigorous techniques for the specification, development, analysis, and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.
A Petri net, also known as a place/transition net, is one of several mathematical modeling languages for the description of distributed systems. It is a class of discrete event dynamic system. A Petri net is a directed bipartite graph that has two types of elements: places and transitions. Place elements are depicted as white circles and transition elements are depicted as rectangles. A place can contain any number of tokens, depicted as black circles. A transition is enabled if all places connected to it as inputs contain at least one token. Some sources state that Petri nets were invented in August 1939 by Carl Adam Petri—at the age of 13—for the purpose of describing chemical processes.
In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification. This is typically associated with hardware or software systems, where the specification contains liveness requirements as well as safety requirements.
In computer science, the process calculi are a diverse family of related approaches for formally modelling concurrent systems. Process calculi provide a tool for the high-level description of interactions, communications, and synchronizations between a collection of independent agents or processes. They also provide algebraic laws that allow process descriptions to be manipulated and analyzed, and permit formal reasoning about equivalences between processes. Leading examples of process calculi include CSP, CCS, ACP, and LOTOS. More recent additions to the family include the π-calculus, the ambient calculus, PEPA, the fusion calculus and the join-calculus.
In computer science, concurrency is the ability of different parts or units of a program, algorithm, or problem to be executed out-of-order or in partial order, without affecting the outcome. This allows for parallel execution of the concurrent units, which can significantly improve overall speed of the execution in multi-processor and multi-core systems. In more technical terms, concurrency refers to the decomposability of a program, algorithm, or problem into order-independent or partially-ordered components or units of computation.
The actor model in computer science is a mathematical model of concurrent computation that treats an actor as the basic building block of concurrent computation. In response to a message it receives, an actor can: make local decisions, create more actors, send more messages, and determine how to respond to the next message received. Actors may modify their own private state, but can only affect each other indirectly through messaging.
The CO-OPN specification language is based on both algebraic specifications and algebraic Petri nets formalisms. The former formalism represent the data structures aspects, while the latter stands for the behavioral and concurrent aspects of systems. In order to deal with large specifications some structuring capabilities have been introduced. The object-oriented paradigm has been adopted, which means that a CO-OPN specification is a collection of objects which interact concurrently. Cooperation between the objects is achieved by means of a synchronization mechanism, i.e., each object event may request to be synchronized with some methods of one or a group of partners by means of a synchronization expression.
In computer science, the Actor model and process calculi are two closely related approaches to the modelling of concurrent digital computation. See Actor model and process calculi history.
A Kahn process network is a distributed model of computation in which a group of deterministic sequential processes communicate through unbounded first in, first out channels. The model requires that reading from a channel is blocking while writing is non-blocking. Due to these key restrictions, the resulting process network exhibits deterministic behavior that does not depend on the timing of computation nor on communication delays.
In computer science, the Actor model, first published in 1973, is a mathematical model of concurrent computation.
In computer science, the Actor model, first published in 1973, is a mathematical model of concurrent computation. This article reports on the later history of the Actor model in which major themes were investigation of the basic power of the model, study of issues of compositionality, development of architectures, and application to Open systems. It is the follow on article to Actor model middle history which reports on the initial implementations, initial applications, and development of the first proof theory and denotational model.
YAWL is a workflow language based on workflow patterns. It is supported by a software system that includes an execution engine, a graphical editor and a worklist handler. It is available as open-source software under the LGPL license.
Enterprise engineering is the body of knowledge, principles, and practices used to design all or part of an enterprise. An enterprise is a complex socio-technical system that comprises people, information, and technology that interact with each other and their environment in support of a common mission. One definition is: "an enterprise life-cycle oriented discipline for the identification, design, and implementation of enterprises and their continuous evolution", supported by enterprise modelling. The discipline examines each aspect of the enterprise, including business processes, information flows, material flows, and organizational structure. Enterprise engineering may focus on the design of the enterprise as a whole, or on the design and integration of certain business components.
An algebraic Petri net (APN) is an evolution of the well known Petri net in which elements of user defined data types replace black tokens. This formalism can be compared to coloured Petri nets (CPN) in many aspects. However, in the APN case, the semantics of the data types is given by an axiomatization enabling proofs and computations on it.
TAPAAL is a tool for modelling, simulation and verification of Timed-Arc Petri nets developed at Department of Computer Science at Aalborg University in Denmark and it is available for Linux, Windows and Mac OS X platforms.
Subject-oriented business process management (S-BPM) is a communication based view on actors, which compose a business process orchestration or choreography. The modeling paradigm uses five symbols to model any process and allows direct transformation into executable form.
Rüdiger Valk is a German mathematician. From 1976 to 2010 he was Professor for Theoretical Computer Science (Informatics) at the Institut für Informatik of the University of Hamburg, Germany.
In computer science, especially model checking and abstract interpretation, widening refers to at least two different techniques in the analysis of abstract transition systems where infinite progressions of abstract states are replaced by a least fixed point. The use of the term in model checking is closely related to acceleration techniques, some authors reserving acceleration for exact computations.
Hartmut Ehrig was a German computer scientist and professor of theoretical computer science and formal specification. He was a pioneer in algebraic specification of abstract data types, and in graph grammars.
Signal Transition Graphs (STGs) are typically used in electronic engineering and computer engineering to describe dynamic behaviour of asynchronous circuits, for the purposes of their analysis or synthesis.