FROM PETRI NETS TO LINEAR LOGIC THROUGH CATEGORIES: A SURVEY

1991 ◽  
Vol 02 (04) ◽  
pp. 297-399 ◽  
Author(s):  
NARCISO MARTÍ -OLIET ◽  
JOSÉ MESEGUER
Keyword(s):  
Petri Nets ◽  
Linear Logic ◽  
Concurrent Systems ◽  
The Other ◽  
Axiomatic Treatment ◽  
Computational Perspective ◽  
Concurrent Computation ◽  
Categorical Models ◽  
The One ◽  
Categorical Semantics

Linear logic has been introduced by Girard as a logic of actions that seems well suited for concurrent computation. This paper surveys recent work on the applications of linear logic to concurrency, with special emphasis on Petri nets and on the use of categorical models. In particular, we present a synthesis of our previous work on the systematic correspondence between Petri nets, linear logic theories, and linear categories, and explain its relationships to work by many other authors. Throughout, we discuss the computational interpretation of the linear logic connectives and illustrate the ideas with examples. Categories play an important role in this survey. On the one hand, from a computational perspective, they are interpreted as concurrent systems whose objects are states, and whose morphisms are transitions; on the other hand, when a model-theoretic perspective is adopted, they provide a very flexible conceptual framework within which the relationships among quite different models already proposed for linear logic can be better understood; this framework also suggests the study of new models and an axiomatic treatment of classes of models. Our categorical semantics for linear logic is based on dualizing objects and permits a very simple presentation of ideas requiring a more complicated treatment in the language of *-autonomous categories.

From Petri nets to linear logic

1991 ◽  
Vol 1 (1) ◽  
pp. 69-101 ◽  
Author(s):  
Narciso Martí-Oliet ◽  
José Meseguer
Keyword(s):  
Petri Nets ◽  
Category Theory ◽  
Linear Logic ◽  
Concurrent Systems ◽  
Concurrent Computation

Linear logic has recently been introduced by Girard as a logic of actions that seems well suited for concurrent computation. In this paper, we establish a systematic correspondence between Petri nets, linear logic theories, and linear categories. Such a correspondence sheds new light on the relationships between linear logic and concurrency, and on how both areas are related to category theory. Categories are here viewed as concurrent systems the objects of which are states, and the morphisms of which are transitions. This is an instance of the Lambek-Lawvere correspondence between logic and category theory that cannot be expressed within the more restricted framework of the Curry-Howard correspondence.

THE APPLICATION OF PETRI NETS TO WORKFLOW MANAGEMENT

1998 ◽  
Vol 08 (01) ◽  
pp. 21-66 ◽  
Author(s):  
W. M. P. VAN DER AALST
Keyword(s):  
Petri Nets ◽  
Petri Net ◽  
Business Processes ◽  
State Of The Art ◽  
Workflow Management ◽  
Explicit Representation ◽  
The Other ◽  
Application Domain ◽  
Analysis Techniques ◽  
The One

Workflow management promises a new solution to an age-old problem: controlling, monitoring, optimizing and supporting business processes. What is new about workflow management is the explicit representation of the business process logic which allows for computerized support. This paper discusses the use of Petri nets in the context of workflow management. Petri nets are an established tool for modeling and analyzing processes. On the one hand, Petri nets can be used as a design language for the specification of complex workflows. On the other hand, Petri net theory provides for powerful analysis techniques which can be used to verify the correctness of workflow procedures. This paper introduces workflow management as an application domain for Petri nets, presents state-of-the-art results with respect to the verification of workflows, and highlights some Petri-net-based workflow tools.

scholarly journals On the semantics of place/transition Petri nets

1997 ◽  
Vol 7 (4) ◽  
pp. 359-397 ◽  
Author(s):  
JOSÉ MESEGUER ◽  
UGO MONTANARI ◽  
VLADIMIRO SASSONE
Keyword(s):  
Petri Nets ◽  
The Other ◽  
General Category ◽  
Monoidal Categories ◽  
Other Hand ◽  
Models Of Concurrency ◽  
A Chain ◽  
The One ◽  
Algebraic Domains

Place/transition (PT) Petri nets are one of the most widely used models of concurrency. However, they still lack, in our view, a satisfactory semantics: on the one hand the ‘token game’ is too intensional, even in its more abstract interpretations in terms of nonsequential processes and monoidal categories; on the other hand, Winskel's basic unfolding construction, which provides a coreflection between nets and finitary prime algebraic domains, works only for safe nets. In this paper we extend Winskel's result to PT nets. We start with a rather general category PTNets of PT nets, we introduce a category DecOcc of decorated (nondeterministic) occurrence nets and we define adjunctions between PTNets and DecOcc and between DecOcc and Occ, the category of occurrence nets. The role of DecOcc is to provide natural unfoldings for PT nets, i.e., acyclic safe nets where a notion of family is used to relate multiple instances of the same place. The unfolding functor from PTNets to Occ reduces to Winskel's when restricted to safe nets. Moreover, the standard coreflection between Occ and Dom, the category of finitary prime algebraic domains, when composed with the unfolding functor above, determines a chain of adjunctions between PTNets and Dom.

scholarly journals CAUSAL REVERSIBILITY IN INDIVIDUAL TOKEN INTERPRETATION OF PETRI NETS

2020 ◽  
Vol 21 (4) ◽  
Author(s):  
Adel Benamira
Keyword(s):  
Petri Nets ◽  
Arbitrary Order ◽  
Concurrent Systems ◽  
The Other ◽  
Initial State

Causal reversibility in concurrent systems means that events that the origin of other events can only be undone after undoing of its consequences. In opposite to backtracking, the events which are independent of each other can be reversed in an arbitrary order, in the other words, we have flexible reversibility w.r.t the causality relation. An implementation of Individual token interpretation ofPetri Nets (IPNs) was been proposed by Rob Van Glabbeek et al, the present paper investigates into a study of causal reversibility within IPNs. Given N be an IPN, by adding an intuitive firing rule to undo transitions according to the causality relation, the coherence of N is assured, i.e., the set of all reachable states of N in the reversible version and that of the original one are identical. Furthermore, reversibility in N is flexible and their initial state can be accessible in reverse from any state. In this paper an approach for controllingcausal-reversibility within IPNs is proposed.

scholarly journals Domain Theory for Concurrency

2003 ◽  
Vol 10 (43) ◽  
Author(s):  
Mikkel Nygaard ◽  
Glynn Winskel
Keyword(s):  
Linear Logic ◽  
Operational Semantics ◽  
Denotational Semantics ◽  
Higher Order ◽  
The Other ◽  
Domain Theory ◽  
Parallel Composition ◽  
Concurrent Computation ◽  
Contextual Equivalence

A simple domain theory for concurrency is presented. Based on a categorical model of linear logic and associated comonads, it highlights the role of linearity in concurrent computation. Two choices of comonad yield two expressive metalanguages for higher-order processes, both arising from canonical constructions in the model. Their denotational semantics are fully abstract with respect to contextual equivalence. One language derives from an exponential of linear logic; it supports a straightforward operational semantics with simple proofs of soundness and adequacy. The other choice of comonad yields a model of affine-linear logic, and a process language with a tensor operation to be understood as a parallel composition of independent processes. The domain theory can be generalised to presheaf models, providing a more refined treatment of nondeterministic branching. The article concludes with a discussion of a broader programme of research, towards a fully fledged domain theory for concurrency.

A Linear Metalanguage for Concurrency

1998 ◽  
Vol 5 (31) ◽  
Author(s):  
Glynn Winskel
Keyword(s):  
Linear Logic ◽  
Higher Order ◽  
The Other ◽  
Order Process ◽  
Open Problems ◽  
Concurrent Process ◽  
Open Map ◽  
Pi Calculus ◽  
Categorical Models ◽  
Future Work

A metalanguage for concurrent process languages is introduced.<br />Within it a range of process languages can be defined, including<br />higher-order process languages where processes are passed and received as arguments. (The process language has, however, to be linear, in the sense that a process received as an argument can be run at most once, and not include name generation as in the Pi-Calculus.) The metalanguage is provided with two interpretations both of which can be understood as categorical models of a variant of linear logic. One interpretation is in a<br />simple category of nondeterministic domains; here a process will denote its set of traces. The other interpretation, obtained by direct analogy with the nondeterministic domains, is in a category of presheaf categories; the nondeterministic branching behaviour of a process is captured in its denotation as a presheaf. Every presheaf category possesses a notion of (open-map) bisimulation, preserved by terms of the metalanguage. The<br />conclusion summarises open problems and lines of future work.

Algebraic high-level net transformation systems

1995 ◽  
Vol 5 (2) ◽  
pp. 217-256 ◽  
Author(s):  
Julia Padberg ◽  
Hartmut Ehrig ◽  
Leila Ribeiro
Keyword(s):  
Petri Nets ◽  
The Other ◽  
Graph Grammars ◽  
Data Types ◽  
Algebraic Specifications ◽  
Categorical Framework ◽  
The One ◽  
High Level ◽  
Transformation Systems ◽  
Dining Philosophers

The concept of algebraic high-level net transformation systems combines two important lines of research recently introduced in the literature:algebraic high-level nets(AHL-nets for short) andhigh-level replacement systems(HLR-systems for short). In both cases a categorical formulation of the corresponding theory has turned out to be highly important and is also a good basis for the integration of these concepts in this paper.AHL-nets combine Petri nets with algebraic specifications and provide a powerful specification technique for distributed systems including data types and processes.HLR-systems are transformation systems for high-level structures such as graphs, hypergraphs, algebraic specifications and different kinds of Petri nets. The theory of HLRsystems - formulated already in a categorical framework - is applied in this paper to AHLnets. Thus we obtain AHL-net transformation systems as an instantiation of HLR-systems to AHL-nets. This allows us to build up AHL-nets from basic components and to transform the net structure using rules or productions in the sense of graph grammars. This concept is illustrated by extending the well-known example of ‘dining philosophers’. We are able to show that AHL-net-transformation systems satisfy several important compatibility properties. On the one hand we obtain a local Church-Rosser and Parallelism Theorem, which is well-known for graph grammars and has recently been generalized to HLR-systems. This allows us to analyse concurrency in AHL-nets not only on the token level but also on the level of transformations of the net structure. On the other hand, we consider the ‘fusion’ and ‘union’ constructions for high-level structures, motivated by corresponding concepts for high-level Petri nets in the literature, and we show compatibility of these constructions with derivations of HLR-systems in general and AHL-nettransformations in particular. This means compatibility of vertical and horizontal structuring in terms of software development.

scholarly journals Coloured Petri Nets Extended with Place Capacities, Test Arcs and Inhibitor Arcs

1992 ◽  
Vol 21 (398) ◽  
Author(s):  
Søren Christensen ◽  
Niels Damgaard Hansen
Keyword(s):  
Petri Nets ◽  
Petri Net ◽  
The Other ◽  
Coloured Petri Nets ◽  
Basic Properties ◽  
New Concepts ◽  
Special Cases ◽  
The One ◽  
Net Framework ◽  
Informal Description

In this paper we show how to extend Coloured Petri Nets (CP-nets), with three new modelling primitives - place capacities, test arcs and inhibitor arcs. The new modelling primitives are introduced to improve the possibilities of creating models that are on the one hand compact and comprehensive and on the other hand easy to develop, understand and analyse. A number of different place capacity and inhibitor concepts have been suggested earlier, e.g. integer and multi-set capacities and zero-testing and threshold inhibitors. These concepts can all be described as special cases of the more general place capacity and inhibitor concepts defined in this paper. We give an informal description of the new concepts and show how the concepts can be fonnally defined and integrated in the Petri net framework keeping the basic properties of CP-nets. In contrast to a number of the previously suggested extensions to CP-nets the new modelling primitives preserve the concurrency properties of CP-nets. We show how CP-nets with place capacities, test arcs and inhibitor arcs can be transformed into behaviourally equivalent CP-nets without these primitives. From this we conclude that the basic properties of CP-nets are preserved and that the theory developed for CP-nets can be applied to the extended CP-nets. Finally, we discuss how to generalise the analysis methods of CP-nets to cover the place capacities, test arcs and inhibitor arcs.

Note on Selection of Coordinate Systems for Geodynamics

1975 ◽  
Vol 26 ◽  
pp. 395-407
Author(s):  
S. Henriksen
Keyword(s):  
Sea Level ◽  
The Other ◽  
Coordinate Systems ◽  
Mean Sea Level ◽  
The Earth ◽  
The One ◽  
Static Systems ◽  
Selection Of

The first question to be answered, in seeking coordinate systems for geodynamics, is: what is geodynamics? The answer is, of course, that geodynamics is that part of geophysics which is concerned with movements of the Earth, as opposed to geostatics which is the physics of the stationary Earth. But as far as we know, there is no stationary Earth – epur sic monere. So geodynamics is actually coextensive with geophysics, and coordinate systems suitable for the one should be suitable for the other. At the present time, there are not many coordinate systems, if any, that can be identified with a static Earth. Certainly the only coordinate of aeronomic (atmospheric) interest is the height, and this is usually either as geodynamic height or as pressure. In oceanology, the most important coordinate is depth, and this, like heights in the atmosphere, is expressed as metric depth from mean sea level, as geodynamic depth, or as pressure. Only for the earth do we find “static” systems in use, ana even here there is real question as to whether the systems are dynamic or static. So it would seem that our answer to the question, of what kind, of coordinate systems are we seeking, must be that we are looking for the same systems as are used in geophysics, and these systems are dynamic in nature already – that is, their definition involvestime.

Stories and the Self

2020 ◽  
Vol 32 (2) ◽  
pp. 47-58 ◽  
Author(s):  
Stefan Krause ◽  
Markus Appel
Keyword(s):  
Meta Analysis ◽  
The Self ◽  
The Other ◽  
Lower Degree ◽  
Contrast Effects ◽  
Self Perception ◽  
Self Perceptions ◽  
Other Hand ◽  
The One ◽  
Implicit And Explicit

Abstract. Two experiments examined the influence of stories on recipients’ self-perceptions. Extending prior theory and research, our focus was on assimilation effects (i.e., changes in self-perception in line with a protagonist’s traits) as well as on contrast effects (i.e., changes in self-perception in contrast to a protagonist’s traits). In Experiment 1 ( N = 113), implicit and explicit conscientiousness were assessed after participants read a story about either a diligent or a negligent student. Moderation analyses showed that highly transported participants and participants with lower counterarguing scores assimilate the depicted traits of a story protagonist, as indicated by explicit, self-reported conscientiousness ratings. Participants, who were more critical toward a story (i.e., higher counterarguing) and with a lower degree of transportation, showed contrast effects. In Experiment 2 ( N = 103), we manipulated transportation and counterarguing, but we could not identify an effect on participants’ self-ascribed level of conscientiousness. A mini meta-analysis across both experiments revealed significant positive overall associations between transportation and counterarguing on the one hand and story-consistent self-reported conscientiousness on the other hand.

Sign in / Sign up

Export Citation Format

Share Document