A Selection of Papers from CONCUR 2010

As I have already mentioned in earlier posts, I enjoyed a lot of talks in the programme for CONCUR 2010. Here are just a few highlights, with apologies to all the speakers whose talks/papers I do not mention in this post. Overall, the conference programme was of very high quality. This bodes well for the future of CONCUR.

• Lutz Schröder and Yde Venema. Flat Coalgebraic Fixed Point Logic. Lutz presented the paper and gave a very clear introduction to the coalgebraic approach to the study of modal logics. Technically, this paper presents a unified co-algebraic treatment  of flat fixed-point logics. (Fixed-point logics, such as the mu-calculus, are widely used in computer science, in particular in artificial intelligence and concurrency.) The main results in the paper are the completeness of the Kozen-Park axiomatization and a general  EXPTIME upper bound for flat fixed-point logics.
• Fides Aarts and Frits Vaandrager. Learning I/O Automata. The talk was delivered by Frits, who addressed the general question of learning models of reactive systems automatically, e.g., for model-based testing or software engineering.In this work, Fides and Frits establish links between three widely used modelling frameworks for reactive systems: the ioco theory of Tretmans, the interface automata of De Alfaro and Henzinger, and Mealy machines. It is shown that, by exploiting these links, any tool for active learning of Mealy machines can be used for learning I/O automata that are deterministic and output determined. The approach presented in the paper has been implemented on top of the LearnLib tool and has been applied successfully to three case studies, including learning a model of Fides' biometric passport. 
• Pawel Sobocinski. Representations of Petri net interactions. . Pawel, who was my co-chair for SOS 2010, presented a novel compositional algebra of Petri nets. The algebra contains two binary operators (tensor product and sequential composition) and twelve constants! He also introduced a stateful extension of the calculus of connectors and showed that .these two formalisms have the same expressive power.
• Pavol Cerny, Thomas Henzinger and Arjun Radhakrishna. Simulation Distances.  The simulation preorder is often used to establish the correctness of an implementation I with respect to a specification S as follows: I correctly implements S if S can simulate the behaviour of I. In other words, this happens if everything the implementation I does is allowed by the specification S. The result of such a verification is boolean and cannot be used to assess how far I is from implementing the behaviour allowed by  S. This paper extends the simulation preorder to the quantitative setting by  defining three different simulation distances. The correctness distance measures how much the specification must be changed in order to be satisfied by the implementation. The coverage distance measures how much the implementation restricts the degrees of freedom offered by the specification. The robustness distance measures how much a system can deviate from the implementation description without violating the specification. The paper develops a comprehensive theory for those notions of simulation distances. 

Reading the papers from CONCUR 2010 will keep me busy for some time.