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.
The model-checking problem for 1-safe Petri nets and linear-time temporal logic (LTL) consists of deciding, given a 1-safe Petri net and a formula of LTL, whether the Petri net satisfies the property encoded by the formula. This paper introduces a semidecision test for this problem. By a semidecision test we understand a procedure which may answer ‘yes’, in which case the Petri net satisfies the property,...
It is generally admitted that timed models can be obtained as extensions of untimed (discrete) models by adding constructs that allow to manipulate time explicitly or implicitly. For instance, timed automata are automata extended with continuous variables, called clocks, that can be tested and modified at transitions. Timed process algebras are languages obtained by adding constructs such as delays,...
After some general considerations concerning modeling issues, the paper concentrates on the fact that places are generally interpreted as logical conditions. There are various kind of logical propositions, some (the resources) are consumed when they are used in the same way tokens are removed from places when transitions are fired. Linear logic has pointed out the fact that resources had to be handled...
This paper considers the appropriate properties for abstract net components in the Coloured Petri Net formalism. In doing so, it attempts to maintain the duality between places and transitions which is so foundational to Petri Net theory. It also defines what it means to execute the net at an abstract level.
Inheritance is one of the key issues of object-orientation. The inheritance mechanism allows for the definition of a subclass which inherits the features of a specific superclass. This means that methods and attributes defined for the superclass are also available for objects of the subclass. Existing methods for object-oriented modeling and design abstract from the dynamic behavior of objects when...
Based on Y. Shoham's paradigm, called Agent-Oriented Programming (AOP), multi-agent-systems are presented as a specialization of distributed, Object-Oriented systems. Equipped with knowledge, general concurrent inference mechanisms dealing with this knowledge, and a declarative agent program, these multi-agent-systems are intended to be a foundation of a new approach uniting advantages of many contributing...
We study the complexity of model-checking Petri Nets w.r.t. the prepositional linear-time μ-calculus. Esparza has shown in [5] that it is decidable, but the space complexity of his algorithm is exponential in the size of the system and double exponential in the size of the formula. In this paper we show that the complexity in the size of the formula can be reduced to polynomial space. We also prove...
In almost all process algebras the equation ‘P; θ=P’ holds on a semantic level. This is not the case for standard Petri Box Calculus (PBC) We introduce a new structural equivalence ≊θ on labeled nets, based on a reduction of “silent transitions”, noted θ. Consequently, we show that the net semantics implemented in the actual PEP-versions, which ensures minimal size of the nets and 1-safeness,...
The objective of this work is to give Merlin's time Petri nets a partial order semantics based on the nonsequential process semantics for untimed net systems. A time process of a time Petri net is defined as a traditionally constructed causal process whose events are labeled with occurrence times. In a valid timing, the occurrence times satisfy specific criteria that arise from the interaction...
It is well known that Petri nets constitute the algebraic structure of quantales, which can be models of linear logic. As a timed extension to quantales, timed R-monoids are defined, which are constructed from timed Petri nets. Next, temporal linear logic is introduced, which has timed Petri nets as its models, i.e., whose formulas can be interpreted as sets of timed markings of a timed Petri net...
We study the introduction of transitions with Phase-type distribution firing time in (bounded) generalized stochastic Petri nets. Such transitions produce large increases of both space and time complexity for the computation of the steady state probabilities of the underlying Markov chain. We propose a new approach to limit this phenomenon while keeping full stochastic semantics of previous works...
Concurrency theory, as developed by Carl Adam Petri, is an axiomatic theory of binary relations of concurrency (co) and causality (li). This work deals with interactions between axioms and studies properties of concurrency structures, the models of this theory. In contrast to other treatments concurrency theory will be investigated in its general form, which does not require an underlying partial...
In this paper we propose an efficient reachability set based Petri net analysis by introducing dynamic priorities which decreases the number of reachable markings in most cases. It is proved that for specific dynamic priority relations certain properties (especially liveness and the existence of home states) do hold if and only if these properties do also hold for the Petri net without priorities...
In this paper we introduce the concept of a Petri net component and show how systems can be composed from components. A component communicates with its environment via distinguished input and output places, which formalizes communication by message passing. Then, we present a compositional semantics for components. The semantics is an extension of processes for place/transition systems (partial order...
Within the framework of concurrent systems, several verification approaches require as a preliminary step the complete derivation of the state space. Partial-order methods are efficient for reducing the state explosion due to the modeling of parallelism by interleaving. In the case of persistent or sleep sets, only a subset of enable transitions is examined, the derived graph is then a subgraph...
Commoner's Theorem establishes a relation between siphons, traps and liveness in free choice systems. Most proofs of this theorem do explicitly involve the finiteness of the net. Therefore we cannot apply the theorem directly to high level nets with infinite color domains. We prove generalisations of both the “if” and the “only if” direction to the infinite case which unfortunately cannot be...
This paper is about the two compulsory project assignments set to the students in an undergraduate course on distributed systems. In the first assignment the students design and validate a non-trivial layered protocol by means of Coloured Petri Nets, and in the second they implement the designed protocol in an object-oriented language. From the two assignments the students experience that Coloured...
We here consider transition systems of Elementary Net Systems with inhibitor arcs. There are basically two different types of non-interleaving semantics of such Petri nets, the a-posteriori and a-priori semantics. The former is an instance of the causal partial order semantics, and can be captured using means similar to those developed for ordinary safe nets. The latter is based on an extension of...
A model, called Place Chart Nets (PCN), is presented. It allows the modeling of both asynchronicity and exception handling (preemption). Contrary to State Charts and other reactive models, which are inherently synchronous, PCNs specify a system behavior using partial orders. Contrary to Petri nets, PCNs have a notion of hierarchy. Contrary to other hierarchical models based on Petri net extensions,...
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.