An Observational Theory for Mobile Ad Hoc Networks (full version)

We 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.     

A CPS Encoding of Name-Passing in Higher-Order Mobile Embedded Resources

We present an encoding of the synchronous π-calculus in the calculus of Higher-Order Mobile Embedded Resources (Homer), a pure higher-order calculus with mobile processes in nested locations, defined as a simple, conservative extension of the core process-passing subset of Thomsen's Plain CHOCS. We prove that our encoding is fully abstract with respect to barbed bisimulation and sound with respect to barbed congruence. Our encoding demonstrates that higher-order process-passing together with mobile resources in (local) named locations are sufficient to express π-calculus name-passing. The encoding uses a novel continuation passing style to facilitate the encoding of synchronous communication.     

A CPS encoding of name-passing in Higher-order mobile embedded resources

We present an encoding of the synchronous π$\pi$-calculus in the calculus of Higher-order mobile embedded resources (Homer), a pure higher-order calculus with mobile processes in nested locations, defined as a simple, conservative extension of the core process-passing subset of Thomsen's Plain CHOCS. We prove that our encoding is fully abstract with respect to barbed bisimulation and sound with respect to barbed congruence. Our encoding demonstrates that higher-order process-passing together with mobile resources in, possibly local, named locations are sufficient to express π$\pi$-calculus name-passing. The encoding uses a novel continuation passing style to facilitate the encoding of synchronous communication.     

Basic observables for a calculus for global computing

We develop the semantic theory of a foundational language for modelling applications over global computers whose interconnection structure can be explicitly manipulated. Together with process distribution, process mobility and remote asynchronous communication through distributed data repositories, the language has primitives for explicitly modelling inter-node connections and for dynamically activating and deactivating them. For the proposed language, we define natural notions of extensional observations and study their closure under operational reductions and/or language contexts to obtain barbed congruence and may testing equivalence. We then focus on barbed congruence and provide an alternative characterisation in terms of a labelled bisimulation. To test practical usability of the semantic theory, we model a system of communicating mobile devices and use the introduced proof techniques to verify one of its key properties.     

On the expressiveness and decidability of higher-order process calculi

In higher-order process calculi, the values exchanged in communications may contain processes. A core calculus of higher-order concurrency is studied; it has only the operators necessary to express higher-order communications: input prefix, process output, and parallel composition. By exhibiting a deterministic encoding of Minsky machines, the calculus is shown to be Turing complete. Therefore its termination problem is undecidable. Strong bisimilarity, however, is shown to be decidable. Furthermore, the main forms of strong bisimilarity for higher-order processes (higher-order bisimilarity, context bisimilarity, normal bisimilarity, barbed congruence) coincide. They also coincide with their asynchronous versions. A sound and complete axiomatization of bisimilarity is given. Finally, bisimilarity is shown to become undecidable if at least four static (i.e., top-level) restrictions are added to the calculus.     

Encoding Cryptographic Primitives in a Calculus with Polyadic Synchronisation

We thoroughly study the behavioural theory of epi, a ??-calculus extended with polyadic synchronisation. We show that the natural contextual equivalence, barbed congruence, coincides with early bisimilarity, which is thus its co-inductive characterisation. Moreover, we relate early bisimilarity with the other usual notions, ground, late and open, obtaining a lattice of equivalence relations that clarifies the relationship among the ??standard?? bisimilarities. Furthermore, we apply the theory developed to obtain an expressiveness result: epi extended with key encryption primitives may be fully abstractly encoded in the original epi calculus. The proposed encoding is sound and complete with respect to barbed congruence; hence, cryptographic epi (crypto-epi) gets behavioural theory for free, which contrasts with other process languages with cryptographic constructs that usually require a big effort to develop such theory. Therefore, it is possible to use crypto-epi to analyse and to verify properties of security protocols using equational reasoning. To illustrate this claim, we prove compliance with symmetric and asymmetric cryptographic system laws, and the correctness of a protocol of secure message exchange.     

What is a free name in a process algebra?

There are two popular approaches to specifying the semantics of process algebras: labelled transition semantics and reaction semantics. While the notion of free name is rather unproblematic for labelled transition semantics this is not so for reaction semantics in the presence of a structural congruence for unfolding recursive declarations.We show that the standard definition of free name is not preserved under the structural congruence. We then develop a fixed point approach to the set of free names and show that it is invariant under the structural congruence.     

Finite-valued Semantics for Canonical Labelled Calculi

We define a general family of canonical labelled calculi, of which many previously studied sequent and labelled calculi are particular instances. We then provide a uniform and modular method to obtain finite-valued semantics for every canonical labelled calculus by introducing the notion of partial non-deterministic matrices. The semantics is applied to provide simple decidable semantic criteria for two crucial syntactic properties of these calculi: (strong) analyticity and cut-admissibility. Finally, we demonstrate an application of this framework for a large family of paraconsistent logics.     

‘Closed Interval Process Algebra’ versus ‘Interval Process Algebra’

Summary. In this paper we extend the theory of processes with durational actions that has been proposed in [1,2] to describe and reason about the performance of systems. We associate basic actions with lower and upper time bounds, that specify their possible different durations. Depending on how the lower and upper time bounds are fixed, eager actions (those which happen as soon as they can), lazy actions (those which can wait arbitrarily long before firing) as well as patient actions (those which can be delayed for a while) can be modelled. Processes are equipped with a (soft) operational semantics which is consistent with the original one and is well-timed (observation traces are ordered with respect to time). The bisimulation-based equivalence defined on top of the new operational semantics, timed equivalence, turns out to be a congruence and, within the lazy fragment of the algebra, refines untimed equivalences. Decidability and automatic checking of timed equivalence are also stated by resorting to a finite alternative characterization which is amenable to an automatic treatment by using standard algorithms. The relationships with other timed calculi and equivalences proposed in the literature are also established. Received: 22 May 1998 / 8 November 2000     

Linearity, Persistence and Testing Semantics in the Asynchronous Pi-Calculus

In [C. Palamidessi, V. Saraswat, F. Valencia and B. Victor. On the Expressiveness of Linearity vs Persistence in the Asynchronous Pi Calculus. LICS 2006:59–68, 2006] the authors studied the expressiveness of persistence in the asynchronous π-calculus (Aπ) wrt weak barbed congruence. The study is incomplete because it ignores the issue of divergence. In this paper, we present an expressiveness study of persistence in the asynchronous π-calculus (Aπ) wrt De Nicola and Hennessy's testing scenario which is sensitive to divergence. Following [C. Palamidessi, V. Saraswat, F. Valencia and B. Victor. On the Expressiveness of Linearity vs Persistence in the Asynchronous Pi Calculus. LICS 2006:59–68, 2006], we consider Aπ and three sub-languages of it, each capturing one source of persistence: the persistent-input calculus (PIAπ), the persistent-output calculus (POAπ) and persistent calculus (PAπ). In [C. Palamidessi, V. Saraswat, F. Valencia and B. Victor. On the Expressiveness of Linearity vs Persistence in the Asynchronous Pi Calculus. LICS 2006:59–68, 2006] the authors showed encodings from Aπ into the semi-persistent calculi (i.e., POAπ and PIAπ) correct wrt weak barbed congruence. In this paper we prove that, under some general conditions, there cannot be an encoding from Aπ into a (semi)-persistent calculus preserving the must testing semantics.     

Types and full abstraction for polyadic π-calculus

A type system for terms of the monadic π-calculus is introduced and used to obtain a full-abstraction result for the translation of the polyadic π-calculus into the monadic calculus: well-sorted terms of the polyadic calculus are barbed congruent iff their translations are typed barbed congruent.     

γ演算到Action演算的转换

Action演算簇(action calculi)作为描述不同并发交互行为的数学框架,可以表示一大类具有某些相同特性的并发形式化模型.试图把(演算(一种基于约束的高阶并发计算模)也包含在action演算簇的框架下.首先定义了一个具体的action演算AC(K_γ),然后给出了从(演算到AC(K_γ)转换的形式描述,最后在定义AC(K_γ)的可观察性、弱互模拟关系和弱等价关系的基础上,以(演算为中间表示,证明了这种转换保持了(演算的弱行为等价性.研究表明,action演算簇可以表示基于约束的并发模型,从而充分说明了action演算簇的描述能力,并且为在action演算簇框架下把(演算与其他并发模型结合并进行比较提供了前提.     

Synthesising CCS bisimulation using graph rewriting

The paper presents a case study on the synthesis of labelled transition systems (ltss) for process calculi, choosing as testbed Milner’s Calculus of Communicating System (ccs).The proposal is based on a graphical encoding: each ccs process is mapped into a graph equipped with suitable interfaces, such that the denotation is fully abstract with respect to the usual structural congruence.Graphs with interfaces are amenable to the synthesis mechanism proposed by Ehrig and König and based on borrowed contexts (bcs), an instance of relative pushouts originally introduced by Milner and Leifer.The bc mechanism allows the effective construction of an lts that has graphs with interfaces as both states and labels, and such that the associated bisimilarity is automatically a congruence.Our paper focuses on the analysis of the lts distilled by exploiting the encoding of ccs processes: besides offering major technical contributions towards the simplification of the bc mechanism, a key result of our work is the proof that the bisimilarity on processes obtained via bcs coincides with the standard strong bisimilarity for ccs.     

Coordination by Timers for Channel-Based Anonymous Communications

In this paper we present a new model for timed coordination of communicating distributed processes. The proposed model is an extension of the π-calculus with locations, types, and timers. Types are used to express restricted access to distributed resources. Timers define timeouts for both communication channels and resources. We define the syntax of the model and its operational semantics and provide a few results regarding the typing system and the timers. A timed barbed bisimulation relation is defined to compare the processes. Coordination is given in two stages: by strategically assigning values to timers, and then by employing a set of additional coordination rules. The timed coordination aspects are given through a coordinator pair. It consists of a timers assigning function which can be changed dynamically, and a set of coordination rules. As an illustrating example, we relate our model with the channels of the Reo coordination model.     

A fully abstract semantics for value-passing CCS for trees

We propose a fully abstract semantics for valuepassing CCS for trees (VCCTS) with the feature that processes are located at the vertices of a graph whose edges describe possible interaction capabilities. The operational semantics is given both in terms of a reduction semantics and in terms of a labelled transition semantics. We develop a theory of behavioral equivalences by introducing both weak barbed congruence and weak bisimilarity. In particular, we show that, on image-finite processes, weak barbed congruence coincides with weak bisimilarity. To illustrate potential applications and the powerful expressiveness of VCCTS, we formally compare VCCTS with some well-known models, e.g., dynamic pushdown networks, top-down tree automata and value-passing CCS.     

Towards a theory of bisimulation for the higher-order process calculi

In this paper, a labelled transition semantics for higher-order process calculi is studied. The labelled transition semantics is relatively clean and simple, and corresponding bisimulation equivalence can be easily formulated based on it. And the congruence properties of the bisimulation equivalence can be proved easily. To show the correspondence between the proposed semantics and the well-established ones, the bisimulation is characterized as a version of barbed equivalence and a version of context bisimulation.     

Lower-bound-constrained runs in weighted timed automata

We investigate a number of problems related to infinite runs of weighted timed automata (with a single weight variable), subject to lower-bound constraints on the accumulated weight. Closing an open problem from Bouyer et al. (2008), we show that the existence of an infinite lower-bound-constrained run is—for us somewhat unexpectedly—undecidable for weighted timed automata with four or more clocks.This undecidability result assumes a fixed and known initial credit. We show that the related problem of existence of an initial credit for which there exists a feasible run is decidable in PSPACE. We also investigate the variant of these problems where only bounded-duration runs are considered, showing that this restriction makes our original problem decidable in  NEXPTIME. We prove that the universal versions of all those problems (i.e, checking that all the considered runs satisfy the lower-bound constraint) are decidable in PSPACE.Finally, we extend this study to multi-weighted timed automata: the existence of a feasible run becomes undecidable even for bounded duration, but the existence of initial credits remains decidable (in PSPACE).