1,721,038 research outputs found
An Observational Theory for Mobile Ad Hoc Networks (full version)
No full textAbstractWe propose a process calculus to study the behavioural theory of Mobile Ad Hoc Networks. The operational semantics of our calculus is given both in terms of a Reduction Semantics and in terms of a Labelled Transition Semantics. We prove that the two semantics coincide. The labelled transition system is then used to derive the notions of (weak) simulation and bisimulation for ad hoc networks. The labelled bisimilarity completely characterises reduction barbed congruence, a standard branching-time and contextually-defined program equivalence. We then use our (bi)simulation proof method to formally prove a number of non-trivial properties of ad hoc networks
An Observational Theory for Mobile Ad Hoc Networks
No full textAbstractWe propose a process calculus to study the observational theory of Mobile Ad Hoc Networks. The operational semantics of our calculus is given both in terms of a Reduction Semantics and in terms of a Labelled Transition Semantics. We prove that the two semantics coincide. The labelled transition system is then used to derive the notions of simulation and bisimulation for ad hoc networks. As a main result, we prove that the (weak) labelled bisimilarity completely characterises (weak) reduction barbed congruence, a standard, branching-time, contextually-defined program equivalence. We then use our (bi)simulation proof methods to formally prove a number of non-trivial properties of ad hoc networks
On the Expressiveness of Chi, Update, and Fusion calculi
No full textAbstractChi and Update calculi [9,17] have been independently introduced in order to model mobile systems. The two calculi are very close to each other and represent an evolution of π-calculus [15]. More recently a (non-straightforward) polyadic version of the Update calculus, the Fusion calculus, has been proposed [18].In the paper we give a fully abstract encoding from an asynchronous variant of Chi and Update calculi to asynchronous π-calculus [11,4]. This proves that, at least for their asynchronous variants, Chi and Update calculi are not more expressive than π-calculus. A similar result can be proved for the Fusion calculus
On the observational theory of the CPS-calculus
No full textWe apply powerful proof-techniques of concurrency theory to study the observational theory of Thielecke’s CPS-calculus, a distillation of the target language of Continuation-Passing Style transforms. We define a labelled transition system from which we derive a (weak) labelled bisimilarity that completely characterises Morris’ context-equivalence. We prove a context lemma showing that Morris’ context-equivalence coincides with a simpler context-equivalence closed under a smaller class of contexts. Then we profit of the determinism of the CPS-calculus to give a simpler labelled characterisation of Morris’ equivalence, in the style of Abramsky’s applicative bisimilarity. We enhance our bisimula- tion proof-methods with up to bisimilarity and up to context proof techniques. We use our bisimulation proof techniques to investigate a few algebraic properties on diverging terms that cannot be proved using the original axiomatic semantics of the CPS-calculus
On the Observational Theory of the CPS-calculus (Extended Abstract)
No full textAbstractWe study the observational theory of Thielecke's (recursive) CPS-calculus, a target language for CPS transforms designed to bring out the jumping, imperative nature of continuation-passing.We define a labelled transition system for the CPS-calculus from which we derive a (weak) labelled bisimilarity that completely characterises Morris' context-equivalence. We prove a context lemma showing that Morris' context-equivalence coincides with a simpler context-equivalence closed under a certain class of contexts. Then we profit of the determinism of the CPS-calculus to give a simpler labelled characterisation of Morris' equivalence, resembling Abramsky's applicative bisimilarity. We enhance our bisimulation proof-methods with up-to bisimilarity and up-to context proof techniques. We use our bisimulation proof techniques to study the algebraic theory of the CPS-calculus proving two new algebraic laws that we conjecture cannot be derived using the original axiomatic semantics for the CPS-calculus. Finally, we prove the full abstraction of Thielecke's encoding of the CPS-calculus into a fragment of Fournet and Gonthier's Join-calculus with single pattern definitions
A semantic analysis of key management protocols for wireless sensor networks
Full text linkGorrieri and Martinelli's timed Generalized Non-Deducibility on Compositions (tGNDC) schema is a well-known general framework for the formal verification of security protocols in a concurrent scenario. We generalise the tGNDC schema to verify wireless network security protocols. Our generalisation relies on a simple timed broadcasting process calculus whose operational semantics is given in terms of a labelled transition system which is used to derive a standard simulation theory. We apply our tGNDC framework to perform a security analysis of three well-known key management protocols for wireless sensor networks: μTESLA, LEAP+ and LiSP
On asynchrony in name-passing calculi
No full textWe study an asynchronous pi-calculus, called Local pi (Lpi), where: (a) only the output capability of names may be transmitted; (b) there is no matching or similar constructs. We study the basic operational and algebraic theory of Lpi and show some applications: the derivability of delayed input; the correctness of an optimisation of the encoding of call-by-name lambda-calculus; the validity of some laws for the Join-calculus
A Semantic Theory of the Internet of Things (extended abstract)
Full text linkWe propose a process calculus for modelling and reasoning on systems in the Internet of Things paradigm. Our systems interact both with the physical environment, via sensors and actuators, and with smart devices, via short-range and Internet channels. The calculus is equipped with a standard notion of labelled bisimilarity which represents a fully abstract characterisation of a well-known contextual equivalence. We use our semantic proof-methods to prove run-time properties of a non-trivial case study as well as system equalities
Locality and Polyadicity in Asynchronous Name-Passing Calculi
Full text linkWe give a divergence-free encoding of polyadic Local pi into its monadic variant. Local pi is a sub-calculus of asynchronous pi-calculus where the recipients of a channel are local to the process that has created the channel. We prove the encoding fully-abstract with respect to barbed congruence. This implies that in Local pi (i) polyadicity does not add extra expressive power, and (ii) when studying the theory of polyadic Local pi we can focus on the simpler monadic variant. Then, we show how the idea of our encoding can be adapted to name-passing calculi with non-binding input prefix, such as Chi , Fusion and piF calculi
On Equators in Asynchronous Name-passing Calculi without Matching (Extended Abstract)
No full textWe give a labeled characterization of barbed congruence in asynchronous -calculus, which, unlike previous characterizations, does not use the matching construct. In absence of matching the observer cannot directly distinguish two names. In asynchronous -calculus the fact that two names are indistinguishable can be modeled by means of Honda and Yoshida's notion of equator. Our labeled characterization is based on such a notion. As an application of our theory we provide a fully abstract encoding w.r.t. barbed congruence of external mobility (communication of free names) in terms of internal mobility (communication of private names)
- …
