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
]
Thu Jul 31 18:52:56 CEST 2003
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 ContextFree Processes is EXPTIMEhard
Richard Mayr
Event Structures for Interrupt Process Algebras
Harald Fecher
On the representation of McCarthy's Amb in the picalculus
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 FailuresBased 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 ContextFree Processes is EXPTIMEhard
Richard Mayr, Department of Computer Science, AlbertLudwigsUniversity Freiburg
We show that checking weak bisimulation equivalence of two contextfree processes (also called BPAprocesses) is EXPTIMEhard, even under the condition that the processes are normed. Furthermore, checking weak regularity (finiteness up to weak bisimilarity) for contextfree processes is EXPTIMEhard as well. Adding a finite control of the minimal nontrivial size of 2 to the BPA process already makes weak bisimilarity undecidable.
Keywords: Contextfree 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 picalculus
Arnaud Carayol, IRISA  Rennes, France
Daniel Hirschkoff, ENSLyon, France
Davide Sangiorgi, University of Bologna, Italy
We study the encoding of lambaAMB, the call by name lambdacalculus enriched with McCarthy's AMB operator, into the picalculus. Semantically, AMB is a challenging operator, for the fairness constraints that it expresses. We prove that, under a certain interpretation of divergence in the lambdacalculus (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 lambdacalculi. We then use these methods to derive the most important laws concerning AMB. We take bisimilarity as behavioural equivalence on the picalculus, which sheds some light on the relationship between fairness and bisimilarity. As a spinoff result, we show that there is no smallstep operational semantics for lambaAMB that preserves the branching structure of terms and yields the correct predicates of convergence and (weak) divergence.
Keywords: piicalculus, 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 Turingcomplete 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 FailuresBased 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 fourfold: 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, timeouts, preemption, synchrony and asynchrony. The expressiveness and usefulness of \ntcc has been illustrated by modelling and analysing mutable data structures, valuepassing communication, and applications involving timed systems (RCX controllers), multiagent 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 infinitestate ntcc processes, the ntcc LTL, and for the standard firstorder LTL described by Manna and Pnueli.
email to the webadmin of this site