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 ]

Invited Talks

Nested Semantics over Finite Trees are Equationally Hard Luca Aceto, Aalborg University, DK (based upon joint work with Wan Fokkink, Rob van Glabbeek and Anna Ingolfsdottir) Abstract: One of the criteria that has been put forward for studying the mathematical tractability of the behavioural equivalences in van Glabbeek's linear time-branching time spectrum is that they afford elegant, finite equational axiomatizations over fragments of process algebraic languages. A review of existing complete equational axiomatizations for many of the behavioural semantics in van Glabbeek's spectrum is offered in his encyclopedic chapter in the Handbook of Process Algebra (North-Holland, Amsterdam, 2001). The equational axiomatizations offered ibidem are over the language BCCSP, a common fragment of Milner's CCS and Hoare's CSP suitable for describing finite synchronization trees, and characterize the differences between behavioural semantics in terms of a few revealing axioms. The main omissions in this menagerie of equational axiomatizations for the behavioural semantics in van Glabbeek's spectrum are axiomatizations for 2-nested simulation semantics and possible futures semantics. The relation of 2-nested simulation was introduced by Groote and Vaandrager as the coarsest equivalence included in completed trace equivalence for which the tyft/tyxt format is a congruence format. Possible futures semantics, on the other hand, was proposed by Brookes and Rounds as far back as 1981, and is one of the nested trace equivalences introduced by Hennessy and Milner. In this talk, I shall present, amongst other results, a mathematical answer to the following natural question: Why have these semantics not been given complete axiomatizations yet, even for the language of finite synchronization trees? More precisely, I shall argue that the 2-nested simulation and the possible futures preorder and equivalence do not admit a finite (in)equational axiomatization over the language BCCSP. I then generalize these negative results to show that, for n>=2, none of the n-nested simulation or trace preorders and equivalences defined by Groote and Vaandrager, and Hennessy and Milner, respectively, afford finite equational axiomatizations over the language BCCSP. Interestingly, the intersection of all of the n-nested simulation or trace equivalences or preorders over image-finite labelled transition systems, and therefore over the language BCCSP, is bisimulation equivalence. Hennessy and Milner proved that bisimulation equivalence is axiomatized over the language BCCSP by means of four classic equations. It follows that this fundamental behavioural equivalence, albeit finitely based over BCCSP, is the limit of sequences of relations that do not afford finite equational axiomatizations themselves. Thus ``finite axiomatizability'' is an example from process theory of a ``discontinuous'' property of a behavioural equivalence---i.e., of a property that ``appears at the limit'', but is not afforded by its finite approximations. Keywords: Concurrency, process algebra, BCCSP, nested simulation, possible futures, nested trace semantics, equational logic, complete axiomatizations, non-finitely based algebras, Hennessy-Milner logic.

Distributed Agreement and its Relation with Error-Correcting Codes Michel Raynal, IRISA, FR (joint work with Roy Friedman, Achour Mostefaoui and Sergio Rajsbaum) Abstract: The "condition based" approach identifies sets of input vectors (called conditions), for which it is possible to design a protocol solving a distributed problem despite process crashes. This talk investigates two related agreement problems, namely consensus and interactive consistency, in the context of the condition-based approach. In consensus, processes have to agree on one of the proposed values; in interactive consistency, they have to agree on the vector of proposed values. For both consensus and interactive consistency, a direct correlation between these problems and error correcting codes is established. In particular, crash failures in distributed agreement problems correspond to erasure failures in error correcting codes, and Byzantine and value domain faults correspond to corruption errors. Keywords: Asynchronous Distributed System, Code Theory, Condition, Consensus, Crash Failure, Distributed Computing, Erroneous Value, Error-Correcting Code, Fault-Tolerance, Hamming Distance, Interactive Consistency.

e-mail to the webadmin of this site