September 26, 2005

A one-day symposium on Semantics of Concurrency will be organized on 26th of September at Eindhoven University of Technology.

09.30 - 10.15 Luca Aceto (Reykjavik University and Aalborg University): Bisimilarity is not Finitely Based over BPA with Interrupt abstract

10:15 - 11:00 Jos Baeten (TU/e): Regular Expressions under Bisimulation abstract

11.00 - 11.15 Coffee/Tea Break

11.15 - 12.00 Wan Fokkink (Vrije Universiteit Amsterdam and CWI): Divide and Congruence abstract

12.00 - 13.00 Lunch Break

13.00 - 13.45 Frits Vaandrager (Radboud Universiteit Nijmegen): Urgency in Timed I/O Automata abstract

13:45 - 14:30 Gordon Plotkin (University of Edinburgh): Hennessy-Plotkin-Brookes Revisited abstract

14:30 - 15:00 Michel Chaudron (TU/e): SACC Project abstract

16:00 - 17:30 Mohammad Mousavi will defend his thesis titled: Structuring Structural Operational Semantic

The OAS group provides financial support for the symposium. Hence, registration will be free of charge. For organizational issues, all participants are asked to send an email before 20th of September to "m.r.mousavi atsign tue.nl" to register for this event.

Directions to the TU/Eindhoven and to a map of the campus can be found here.

Baeten and Bergstra have studied the equational theory and expressiveness of BPA_delta (the extension of Basic Process Algebra (BPA) with a constant delta to describe "deadlock") enriched with two mode transfer operators, viz. the disrupt and interrupt operators. In particular, they offered an equational axiomatization of bisimulation equivalence over the resulting extension of the language BPA_delta. This axiomatization is finite, if so is the underlying set of actions---a state of affairs that is most pleasing for process algebraists.

However, the axiomatization of bisimulation equivalence offered by Baeten and Bergstra relies on the use of auxiliary operators. Although the use of auxiliary operators in the axiomatization of behavioral equivalences over process description languages has been well established since Bergstra and Klop's axiomatization of parallel composition using the left and communication merge operators, to my mind, a result like the aforementioned one always begs the question whether the use of auxiliary operators is necessary to obtain a finite axiomatization of bisimulation equivalence.

In this talk, I'll address the above natural question. In particular, I'll focus on BPA enriched with the interrupt operator, and will show that, in the presence of two distinct actions, bisimulation equivalence is NOT finitely based over BPA with the interrupt operator. Moreover, I'll argue that the collection of closed equations over this language is also not finitely based. This result provides evidence that the use of auxiliary operators is indeed necessary in order to obtain a finite axiomatization of bisimulation equivalence over the language studied by Baeten and Bergstra. In sharp contrast to these results, the collection of closed equations over the language BPA enriched with the disrupt operator is finitely based.

We solve an open question of Milner from 1984. We define a set of so-called well-behaved finite automata that, modulo bisimulation equivalence, corresponds exactly to the set of regular expressions, and we show how to determine whether a given finite automaton is in this set. As an application, we consider the star height of regular processes.

Joint work with Flavio Corradini (Universita di Camerino) and Clemens Grabmayer (VU Amsterdam).

The design of distributed systems is a complex task that requires the integration of multiple quality concerns, such as timeliness, reliability & security. The task may be simplified if concerns can be addressed (constructed & understood) in isolation and can be combined into a system.

The Software Architecture = Components + Coordination (SACC) project set out to develop a method for the design of distributed systems that aimed at an architectural separation of concerns. This method consists of two main tracks:

- a method of modelling & reasoning of concerns and their composition,
- an architecture that shows the feasability of the separation of concerns.

In this talk I will reflect on the results of the project.

Congruence formats for structural operational semantics have been developed for several behavioural equivalences, e.g., bisimulation (Groote & Vaandrager '90), failure equivalence (De Simone '85) and trace equivalence (Bloom '94). These formats impose syntactic restrictions on transition rules, which ensure that the equivalence class of a term f(t1,...,tn) is determined by the equivalence classes of its arguments t1,...,tn. This congruence property is, for instance, essential in order to fit the equivalence into an axiomatic framework.

In this talk it is explained how to derive congruence formats for behavioural equivalences by a careful study of their modal characterizations. Using this technique, we have determined new congruence formats for a whole range of behavioural equivalences.

This is joint work with Bard Bloom, Rob van Glabbeek and Paulien de Wind.

Hennessy and Plotkin gave a domain-theoretic semantics fully abstract for the SIP (Simple Imperative Language) + parallelism + a certain somewhat unnatural construct, but not, unfortunately, abstract without it. Later, Brookes gave a fully-abstract trace semantics for a slight variation on SIP + parallelism. In his semantics, meanings of prgrams are sets of traces subject to certain closure conditions, namely "stuttering" and "mumbling"; traces are sequences of pairs of states.

We revisit these reults in the light of the recent Plotkin-Power algebraic theory of effects, where one considers semantic domains as free algebras for equational theories of the operations giving rise to the effects at hand. The original Hennessy-Plotkin semantics can be given by such a theory and is also isomorphic to a trace semantics where one does not impose closure conditions. It turns out that one can recover (a slight variant of) Brookes' semantics, by adding natural equations, corresponding in a 1-1 manner to (a slight variant of) the closure conditions on traces.

Sifakis et al advocate the use of deadline predicates for the specification of progress properties of Alur-Dill style timed automata. In this talk, we extend these ideas to a more general setting, which may serve as a basis for deductive verification techniques. More specifically, we extend the TIOA framework of Lynch et al with urgency predicates. We identify a suitable language to describe the resulting timed I/O automata with urgency and show that for this language time reactivity holds by construction. We also establish that the class of timed I/O automata with urgency is closed under composition. The use of urgency predicates is compared with three alternative approaches to specifying progress properties that have been advocated in the literature: invariants, stopping conditions and deadlines predicates. We argue that in practice the use of urgency predicates leads to shorter and more natural specifications than any of the other approaches. Some preliminary results on proving invariant properties of timed (I/O) automata with urgency are presented.

Back to top.