EXPRESS'03 10th International Workshop on Expressiveness in Concurrency September 2, 2003 Marseille, France Affiliated with CONCUR 2003, 3 - 5 September 2003.
Invited speakers: Luca Aceto (Aalborg University, DK) Michel Raynal (IRISA , FR)
[ Home | Invited Talks | Call for Papers | Accepted Papers | Preliminary Programme | Online Publication ]

Accepted Papers

Out of 29 submissions, the following 9 papers were accepted by the programme committee.

Expressive Power of Hybrid Systems with Variables, Parameters and Arrays Ruggero Lanotte Adjuncts elimination in the static ambient logic Etienne Lozes Weak Bisimilarity and Regularity of Context-Free Processes is EXPTIME-hard Richard Mayr Event Structures for Interrupt Process Algebras Harald Fecher On the representation of McCarthy's Amb in the pi-calculus Arnaud Carayol, Daniel Hirschkoff, Davide Sangiorgi Axioms for Probability and Nondeterminism Michael Mislove, Joel Ouaknine, James Worrell On the Computational Strength of Pure Ambient Calculi Sergio Maffeis, Iain Phillips A Hierarchy of Failures-Based Models Christie Bolton, Gavin Lowe On the Decidability of Timed Concurrent Constraint Programming (*) Frank Valencia

Expressive Power of Hybrid Systems with Variables, Parameters and Arrays Ruggero Lanotte, Dipartimento di Informatica Universita' di Pisa A hybrid system consists of a finite number of locations, variables and transitions. Different classes are considered in the literature. In this paper we study the different expressive power of these classes. Keywords: expressiveness, Hybrid Systems, integer variables, real variables, arrays, papameters.

Adjuncts elimination in the static ambient logic Etienne Lozes, LIP ENS Lyon The Ambient Logic (AL) has been proposed for expressing spatial properties of processes of the Mobile Ambient calculus (MA). Restricting both the calculus and the logic to their static part yields static ambients (SA) and the static ambient logic (SAL), that form a model for queries about semistructured data. This work adresses the questions of expressiveness and minimality of SAL. We define the intensional fragment of the logic (SALint), the logic without adjuncts, and prove that it captures all the expressiveness of the logic. We moreover establish minimality of SALint. A side contribution of this work is the definition of prenex forms for Gabbay and Pitts' fresh quantifier, which represents a first step towards a notion of normal form for queries. Keywords: Spatial Logics, Concurrency, Semistructured Data, Expressiveness, Minimality

Weak Bisimilarity and Regularity of Context-Free Processes is EXPTIME-hard Richard Mayr, Department of Computer Science, Albert-Ludwigs-University Freiburg We show that checking weak bisimulation equivalence of two context-free processes (also called BPA-processes) is EXPTIME-hard, even under the condition that the processes are normed. Furthermore, checking weak regularity (finiteness up to weak bisimilarity) for context-free processes is EXPTIME-hard as well. Adding a finite control of the minimal non-trivial size of 2 to the BPA process already makes weak bisimilarity undecidable. Keywords: Context-free processes, BPA, bisimulation, weak bisimulation, complexity

Event Structures for Interrupt Process Algebras Harald Fecher, Universität Mannheim, Fakultät für Mathematik und Informatik Interruption is a useful feature in programming and specification languages. Therefore, process algebras has been extended with an additional interrupt operator. We invent a class of event structures, called interrupt event structures, to give a true concurrent semantic to process algebras containing interruption. Interrupt event structures are more expressive than other event structures w.r.t. event trace execution. Furthermore, interrupt event structures can also distinguish simultaneous event executions from event interleaving. We show consistency, based on bisimulation, between the operational and the denotational semantics of a process algebra that contains an interrupt operator. Keywords: process algebra, event structures, interruption, consistency, true concurrency

On the representation of McCarthy's Amb in the pi-calculus Arnaud Carayol, IRISA - Rennes, France Daniel Hirschkoff, ENS-Lyon, France Davide Sangiorgi, University of Bologna, Italy We study the encoding of lambaAMB, the call by name lambda-calculus enriched with McCarthy's AMB operator, into the pi-calculus. Semantically, AMB is a challenging operator, for the fairness constraints that it expresses. We prove that, under a certain interpretation of divergence in the lambda-calculus (weak divergence), a faithful encoding is impossible. However, with a different interpretation of divergence (strong divergence), the encoding is possible, and for this case we derive results and coinductive proof methods to reason about lambaAMB that are similar to those for the encoding of pure lambda-calculi. We then use these methods to derive the most important laws concerning AMB. We take bisimilarity as behavioural equivalence on the pi-calculus, which sheds some light on the relationship between fairness and bisimilarity. As a spin-off result, we show that there is no small-step operational semantics for lambaAMB that preserves the branching structure of terms and yields the correct predicates of convergence and (weak) divergence. Keywords: pii-calculus, behavioural equivalences, expressiveness, lambda calculus

Axioms for Probability and Nondeterminism Michael Mislove, Tulane University, Math Departement Joel Ouaknine, Carnegie Mellon University, Computer Science Department James Worrell, Tulane University, Math Department This paper presents a domain model for a process calculus featuring both probabilistic and nondeterministic choice. The former is modelled using the probabilistic powerdomain of Jones and Plotkin, while the latter is modelled by a geometrically convex variant of the Plotkin powerdomain. The main result is to show that the expected laws for probability and nondeterminism are sound and complete with respect to the model.

On the Computational Strength of Pure Ambient Calculi Sergio Maffeis, Imperial College London Iain Phillips, Imperial College London Cardelli and Gordon's calculus of Mobile Ambients has attracted widespread interest as a model of mobile computation. The standard calculus is quite rich, with a variety of operators, together with capabilities for entering, leaving and dissolving ambients. The question arises of what is a minimal Turing-complete set of constructs. Previous work has established that Turing completeness can be achieved without using communication or restriction. We show that it can be achieved merely using movement capabilities (and not dissolution). We also show that certain smaller sets of constructs are either terminating or have decidable termination. Keywords: Mobile Ambients, Turing completeness, termination, decidability.

A Hierarchy of Failures-Based Models Christie Bolton, Oxford University Gavin Lowe, Oxford University In this paper we identify the failures class, a class of semantic models for describing concurrent systems. Each such model records all possible sequences of interaction, and gives some information about subsequent availability. Each model is associated with a predicate that determines how much availability information is recorded. The general contribution of the paper is four-fold: we show that the failures class forms a complete lattice; we identify the relative strengths of models in terms of their defining predicates; we identify those operators for which each model defines a congruence; and we show how refinement in each model can be automatically tested. More concretely, we apply these general results to specific instances of the class. In particular we construct a spectrum showing the relative strengths of four established models and three interesting new models, and we prove that only Roscoe's stable failures and traces models define congruences over the whole language. Keywords: process algebra, semantic models, CSP, stable failures

On the Decidability of Timed Concurrent Constraint Programming (Short Submission) Frank Valencia, Uppsala University The ntcc process calculus is timed concurrent constraint programming (ccp) model for concurrency. The calculus can represent timed concepts such as unit delays, unbounded finite delays, time-outs, pre-emption, synchrony and asynchrony. The expressiveness and usefulness of \ntcc has been illustrated by modelling and analysing mutable data structures, value-passing communication, and applications involving timed systems (RCX controllers), multi-agent systems (the Predator/Prey game), and musical applications (generation of rhythms patterns and controlled improvisation). Furthermore, ntcc is equipped with an LTL to specify timed properties and with an inference system for the verification problem (i.e., for proving whether a given process fulfills a given LTL specification). This abstract reports on new decidability results for infinite-state ntcc processes, the ntcc LTL, and for the standard first-order LTL described by Manna and Pnueli.

e-mail to the webadmin of this site