

Invited speakers:  
[ Home  Invited Talks  Call for Papers  Accepted Papers  Preliminary Programme  Online Publication ] 
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 timebranching 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 (NorthHolland, 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 2nested simulation semantics and possible futures semantics. The relation of 2nested 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 2nested 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 nnested 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 nnested simulation or trace equivalences or preorders over imagefinite 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 equivalencei.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, nonfinitely based algebras, HennessyMilner logic. 
Distributed Agreement and its Relation with ErrorCorrecting 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 conditionbased 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, ErrorCorrecting Code, FaultTolerance, Hamming Distance, Interactive Consistency. 
email to the webadmin of this site 