Accepted Papers Regular Model Checking Made Simple and Efficient Parosh A. Abdulla, Bengt Jonsson, Marcus Nilsson, and Julien d'Orso On Name Generation and Set-Based Analysis in the Dolev-Yao Model Roberto Amadio and Witold Charatonik Widening the Boundary Between Decidable and Undecidable Hybrid Systems Eugene Asarin and Gerardo Schneider Simulation for Continuous-Time Markov Chains Christel Baier, Joost-Pieter Katoen, Holger Hermanns, and Boudewijn Haverkort A Framework for the Analysis of Security Protocols Michele Boreale and Marzia Buscemi Traces, Pomsets, Fairness and Full Abstraction for Communicating Processes Stephen Brookes Orchestrating Transactions in Join Calculus Roberto Bruni, Cosimo Laneve, and Ugo Montanari A First Order Coalgebraic Model of Pi-Calculus Early Observational Equivalence Marzia Buscemi and Ugo Montanari A Spatial Logic for Concurrency (Part II) Luis Caires and Luca Cardelli Decision Algorithms for Probabilistic Bisimulation Stefano Cattani and Roberto Segala Weak Bisimulation is Sound and Complete for PCTL* Josee Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden A Hierarchy of Polynomial-Time Computable Simulations for Automata Kousha Etessami Regular Sets of Pomsets with Autoconcurrency Jean Fanchon and Remi Morin The Fusion Machine Philippa Gardner, Cosimo Laneve, and Lucian Wischik A Calculus of Mobile Resources Jens Chr. Godskesen, Thomas Hildebrandt, and Vladimiro Sassone HOPLA - A Higher-Order Process Language Mikkel Nygaard and Glynn Winskel Network Invariants in Action Yonit Kesten, Amir Pnueli, Elad Shahar, and Lenore Zuck Causality Semantics of Petri Nets with Weighted Inhibitor Arcs H.C.M. Kleijn and M. Koutny Reducing Model Checking from Multi-Valued CTL* to CTL* B. Konikowska and W. Penczek Why is Simulation Harder Than Bisimulation? Antonin Kucera and Richard Mayr On the Decidability of Cryptographic Protocols with Open-Ended Data Structures Ralf Kuesters Local Model Checking Games for Fixed Point Logic with Chop Martin Lange Decidability of Strong Bisimilarity for Timed BPP Slawomir Lasota Safe Realizability of High-Level Message Sequence Charts Markus Lohrey Axiomatizing an Algebra of Step Reactions for Synchronous Languages Gerald Luettgen and Michael Mendler A Decidable Class of Asynchronous Distributed Controllers P. Madhusudan and P.S. Thiagarajan Typing and Subtyping Mobility in Boxed Ambients Massimo Merro and Vladimiro Sassone A Decidable Fixpoint Logic for Time-Outs Maria Sorea Undecidability of Weak Bisimilarity for Pushdown Processes Jiri Srba Using Ambients to Control Resources David Teller, Pascal Zimmer, and Daniel Hirschkoff Alphabet-Based Synchronisation is Exponentially Cheaper Antti Valmari and Antti Kervinen Refinement-Robust Fairness Hagen Völzer

concur02@fi.muni.cz