This volume constitutes the refereed proceedings of the 17th International Conference on Concurrency Theory. Thirty full papers are presented along with three important invited papers. Each of these papers was carefully reviewed by the editors. Topics include model checking, process calculi, minimization and equivalence checking, types, semantics, probability, bisimulation and simulation, real time, and formal languages.

Inhalt
Invited Lectures.- Mapping the Security Landscape: A Role for Language Techniques.- The Saga of the Axiomatization of Parallel Composition.- Rule-Based Modelling of Cellular Signalling.- Contributed Papers.- Making Random Choices Invisible to the Scheduler.- Strategy Logic.- Solving Games Via Three-Valued Abstraction Refinement.- Linear Time Logics Around PSL: Complexity, Expressiveness, and a Little Bit of Succinctness.- On Modal Refinement and Consistency.- Equivalence Checking for Infinite Systems Using Parameterized Boolean Equation Systems.- Decidability Results for Well-Structured Transition Systems with Auxiliary Storage.- A Nice Labelling for Tree-Like Event Structures of Degree 3.- Causal Message Sequence Charts.- Checking Coverage for Infinite Collections of Timed Scenarios.- Is Observational Congruence Axiomatisable in Equational Horn Logic?.- The Must Preorder Revisited.- Topology-Dependent Abstractions of Broadcast Networks.- On the Expressive Power of Global and Local Priority in Process Calculi.- A Marriage of Rely/Guarantee and Separation Logic.- Fair Cooperative Multithreading.- Precise Fixpoint-Based Analysis of Programs with Thread-Creation and Procedures.- Automatic Derivation of Compositional Rules in Automated Compositional Reasoning.- Compositional Event Structure Semantics for the Internal ?-Calculus.- Interpreting a Finitary Pi-calculus in Differential Interaction Nets.- Mobility Control Via Passports.- Coalgebraic Models for Reactive Systems.- Reactive Systems over Directed Bigraphs.- Asynchronous Games: Innocence Without Alternation.- Bisimulation and Logical Preservation for Continuous-Time Markov Decision Processes.- Strategy Synthesis for Markov Decision Processes and Branching-Time Logics.- Timed Concurrent Game Structures.- PushdownModule Checking with Imperfect Information.- Alternating Automata and a Temporal Fixpoint Calculus for Visibly Pushdown Languages.- Temporal Antecedent Failure: Refining Vacuity.