Concurrency cannot be observed, asynchronously

2014 ◽  
Vol 25 (4) ◽  
pp. 978-1004 ◽  
Author(s):  
PAOLO BALDAN ◽  
FILIPPO BONCHI ◽  
FABIO GADDUCCI ◽  
GIACOMA VALENTINA MONREALE
Keyword(s):  
Petri Nets ◽  
Case Studies ◽  
Weak Equivalence ◽  
Asynchronous Systems ◽  
Preliminary Step ◽  
Π Calculus ◽  
Asynchronous Interactions ◽  
Visual Specification

The paper is devoted to an analysis of the concurrent features of asynchronous systems. A preliminary step is represented by the introduction of a non-interleaving extension of barbed equivalence. This notion is then exploited in order to prove thatconcurrency cannot be observedthrough asynchronous interactions, i.e., that the interleaving and concurrent versions of a suitable asynchronous weak equivalence actually coincide. The theory is validated on some case studies, related to nominal calculi (π-calculus) and visual specification formalisms (Petri nets). Additionally, we prove that a class of systems which is deemed (output-buffered) asynchronous, according to a characterization that was previously proposed in the literature, falls into our theory.

scholarly journals Synchrony versus causality in distributed systems

2014 ◽  
Vol 26 (8) ◽  
pp. 1459-1498 ◽  
Author(s):  
KIRSTIN PETERS ◽  
JENS-WOLFHARD SCHICKE-UFFMANN ◽  
URSULA GOLTZ ◽  
UWE NESTMANN
Keyword(s):  
Distributed Systems ◽  
Petri Nets ◽  
Synchronous System ◽  
Π Calculus ◽  
Asynchronous Interactions

Given a synchronous system, we study the question whether – or, under which conditions – the behaviour of that system can be realized by a (non-trivially) distributed and hence asynchronous implementation. In this paper, we partially answer this question by examining the role of causality for the implementation of synchrony in two fundamental different formalisms of concurrency, Petri nets and the π-calculus. For both formalisms it turns out that each ‘good’ encoding of synchronous interactions using just asynchronous interactions introduces causal dependencies in the translation.

Petri nets semantics of π-calculus

2008 ◽  
Vol 3 (3) ◽  
pp. 290-294
Author(s):  
Zhenhua Yu ◽  
Yuanli Cai ◽  
Haiping Xu
Keyword(s):  
Petri Nets ◽  
Π Calculus

scholarly journals Modelling and Analysis of Distributed Program Execution in BETA Using Coloured Petri Nets

1997 ◽  
Vol 26 (513) ◽  
Author(s):  
Jens Bæk Jørgensen ◽  
Kjeld Høyer Mortensen
Keyword(s):  
Petri Nets ◽  
Case Studies ◽  
Object Oriented ◽  
Coloured Petri Nets ◽  
Program Execution ◽  
Shared Resources ◽  
Computer Tools ◽  
Remote Object ◽  
Critical Regions

<p>Recently, abstractions supporting distributed program execution in the object-oriented language BETA have been designed. A BETA object on one computer may invoke a remote object, i.e., an object hosted by another computer. In this project, the formalism of Coloured Petri Nets (CP-nets or CPN) is used to describe and analyse the protocol for remote object invocation. In the first place, we build a model in order to describe, understand, and improve the protocol. Remote object invocation in BETA is modelled on the level of threads (lightweight processes) with emphasis on the competition for access to critical regions and shared resources. Secondly, the model is analysed. It is formally proved that it has a set of desirable properties, e.g., absence of dead markings.</p><p><strong>Topics:</strong> Systemdesign and verfication using nets; higher-level nets models; computer tools for nets; experience with using nets, case studies; application of nets to protocols.</p>

THE USE OF PETRI NETS FOR THE DESIGN AND VERIFICATION OF ASYNCHRONOUS CIRCUITS AND SYSTEMS

1998 ◽  
Vol 08 (01) ◽  
pp. 67-118 ◽  
Author(s):  
ALEX KONDRATYEV ◽  
MICHAEL KISHINEVSKY ◽  
ALEXANDER TAUBIN ◽  
JORDI CORTADELLA ◽  
LUCIANO LAVAGNO
Keyword(s):  
Petri Nets ◽  
State Space ◽  
Formal Specification ◽  
Asynchronous Circuits ◽  
Concurrent Systems ◽  
Special Focus ◽  
Asynchronous Systems ◽  
Design Framework ◽  
Transition Graph ◽  
Signal Transition Graph

Petri nets46,37,45,48 are a powerful formalism for modeling concurrent systems. They are capable of implicitly describing a vast state space by a succinct representation which gracefully captures the notions of causality, concurrency and conflict between events. Petri nets have also been chosen by many authors as a formalism to describe the behavior of asynchronous circuits by interpreting the events as signal transitions, thus coining the term Signal Transition Graph (STG).50,4 A design framework for asynchronous systems involves three main aspects: formal specification, verification and synthesis. In this paper we review the main techniques we have used to cover these aspects in recent years, with a special focus on asynchronous circuits.

Sign in / Sign up

Export Citation Format

Share Document