CONCUR 2006 - Concurrency Theory

Invited Contributions.- Modeling Timed Concurrent Systems.- Some Remarks on Definability of Process Graphs.- Sanity Checks in Formal Verification.- Invited Tutorials.- Welcome to the Jungle: A Subjective Guide to Mobile Process Calculi.- Probability and Nondeterminism in Operational Models of Concurrency.- Model Checking.- A Livelock Freedom Analysis for Infinite State Asynchronous Reactive Systems.- Proving Liveness by Backwards Reachability.- Model Checking Quantified Computation Tree Logic.- Process Calculi.- Liveness, Fairness and Impossible Futures.- Checking a Mutex Algorithm in a Process Algebra with Fairness.- A Complete Axiomatic Semantics for the CSP Stable-Failures Model.- Transition Systems of Elementary Net Systems with Localities.- Minimization and Equivalence Checking.- Operational Determinism and Fast Algorithms.- Minimization, Learning, and Conformance Testing of Boolean Programs.- A Capability Calculus for Concurrency and Determinism.- Types.- A New Type System for Deadlock-Free Processes.- Sortings for Reactive Systems.- Dynamic Access Control in a Concurrent Object Calculus.- Semantics.- Concurrent Rewriting for Graphs with Equivalences.- Event Structure Semantics for Nominal Calculi.- Encoding ?Duce in the ??-Calculus.- Probability.- A Complete Axiomatisation of Branching Bisimulation for Probabilistic Systems with an Application in Protocol Verification.- Probabilistic I/O Automata: Theories of Two Equivalences.- Reachability in Recursive Markov Decision Processes.- Strategy Improvement for Stochastic Rabin and Streett Games.- Bisimulation and Simulation.- Weak Bisimulation Up to Elaboration.- Generic Forward and Backward Simulations.- On Finite Alphabets and Infinite Bases III: Simulation.- Real Time.- Inference of Event-Recording Automata Using Timed Decision Trees.- Controller Synthesis for MTL Specifications.- On Interleaving in Timed Automata.- Formal Languages.- A Language for Task Orchestration and Its Semantic Properties.- Finding Shortest Witnesses to the Nonemptiness of Automata on Infinite Words.- Second-Order Simple Grammars.