CONCUR 2003 - Concurrency Theory: 14th International Conference, Marseille, France, September 3-5, 2003, Proceedings (Lecture Notes in Computer Science (2761))

Annotation This book constitutes the refereed proceedings of the 14th International Conference on Concurrency Theory, CONCUR 2003, held in Marseille, France in September 2003. The 29 revised full papers presented together with 4 invited papers were carefully reviewed and selected from 107 submissions. The papers are organized in topical sections on partial orders and asynchronous systems, process algebras, games, infinite systems, probabilistic automata, model checking, model checking and HMSC, security, mobility, compositional methods and real time, and probabilistic models This Volume Contains The Proceedings Of The 14th International Conference On Concurrencytheory(concur2003)heldinmarseille,france,september3–5, 2003. The Conference Was Hosted By The Universit ́edeprovenceandthela- Ratoire D’informatique Fondamentale De Marseille (lif). The Purpose Of The Concur Conferences Is To Bring Together Researchers, Developers, And Students In Order To Advance The Theory Of Concurrency, And Promote Its Applications. Interest In This Topic Is Continuously Growing, As A Consequence Of The Importance And Ubiquity Of Concurrent Systems And Their Applications, And Of The Scienti?c Relevance Of Their Fundations. The Scope Of The Conference Covers All Areas Of Semantics, Logics, And Veri?cation Techniques For Concurrent Systems. Topics Include Concurrency-related Aspects Of: Models Of Computation And Semantic Domains, Process Algebras, Petri Nets, Event Struc- Res, Real-time Systems, Hybrid Systems, Decidability, Model-checking, Veri?cation And Re?nement Techniques, Term And Graph Rewriting, Distributed Programming, Logic Constraint Programming, Object-oriented Programming, Types Systems And Algorithms, Case Studies, And Tools And Environments For Programming And - Ri?cation. Of The 107 Papers Submitted This Year, 29 Were Accepted For Presentation. Four Invited Talks Were Given At The Conference: On Distributed Monitoring Of Concurrent And Asynchronous Systems By Albert Beneveniste, On Quantitative Veri?cation Via The Mu-calculus By Luca De Alfaro, On Input-output Au- Mata: Basic, Timed, Hybrid, Probabilistic, Dynamic,. . . By Nancy Lynch, And On Composition Of Cryptographic Protocols In A Probabilistic Polynomial-time Process Calculus By Andre Scedrov. Partial Orders And Asynchronous Systems -- Distributed Monitoring Of Concurrent And Asynchronous Systems -- Synthesis Of Distributed Algorithms Using Asynchronous Automata -- Compression Of Partially Ordered Strings -- Process Algebra -- Bundle Event Structures And Ccsp -- Syntactic Formats For Free -- Priority Rewrite Systems For Osos Process Languages -- Games -- Quantitative Verification And Control Via The Mu-calculus -- Playing Games With Boxes And Diamonds -- The Element Of Surprise In Timed Games -- Infinite Systems -- Deciding Bisimilarity Between Bpa And Bpp Processes -- Verification Of Parametric Concurrent Systems With Prioritized Fifo Resource Management -- Probabilistic Automata -- Input/output Automata: Basic, Timed, Hybrid, Probabilistic, Dynamic,... -- A Process-algebraic Language For Probabilistic I/o Automata -- Compositionality For Probabilistic Automata -- Model-checking -- Satisfiability And Model Checking For Mso-definable Temporal Logics Are In Pspace --^ Equivalence Checking Of Non-flat Systems Is Exptime-hard -- Model Checking A Path -- Model-checking And Hmsc -- Multi-valued Model Checking Via Classical Model Checking -- An Extension Of Pushdown System And Its Model Checking Method -- Netcharts: Bridging The Gap Between Hmscs And Executable Specifications -- High-level Message Sequence Charts And Projections -- Security -- Composition Of Cryptographic Protocols In A Probabilistic Polynomial-time Process Calculus -- Unifying Simulatability Definitions In Cryptographic Systems Under Different Timing Assumptions -- Contract Signing, Optimism, And Advantage -- Mobility -- Full Abstraction For Hopla -- Modeling Consensus In A Process Calculus -- Linear Forwarders -- Compositional Methods And Real Time -- Abstract Patterns Of Compositional Reasoning -- Relating Fairness And Timing In Process Algebras -- A Compositional Semantic Theory For Synchronous Component-based Design -- Probabilistic Models --^ Conditional Expectation And The Approximation Of Labelled Markov Processes -- Comparative Branching-time Semantics For Markov Chains -- Quantitative Relations And Approximate Process Equivalences. Roberto Amadio, Denis Lugiez (eds.). Front Matter....Pages - Distributed Monitoring of Concurrent and Asynchronous Systems....Pages 1-26 Synthesis of Distributed Algorithms Using Asynchronous Automata....Pages 27-41 Compression of Partially Ordered Strings....Pages 42-56 Bundle Event Structures and CCSP....Pages 57-71 Syntactic Formats for Free....Pages 72-86 Priority Rewrite Systems for OSOS Process Languages....Pages 87-102 Quantitative Verification and Control via the Mu-Calculus....Pages 103-127 Playing Games with Boxes and Diamonds....Pages 128-143 The Element of Surprise in Timed Games....Pages 144-158 Deciding Bisimilarity between BPA and BPP Processes....Pages 159-173 Verification of Parametric Concurrent Systems with Prioritized FIFO Resource Management....Pages 174-190 Input/Output Automata: Basic, Timed, Hybrid, Probabilistic, Dynamic,.......Pages 191-192 A Process-Algebraic Language for Probabilistic I/O Automata....Pages 193-207 Compositionality for Probabilistic Automata....Pages 208-221 Satisfiability and Model Checking for MSO-Definable Temporal Logics Are in PSPACE....Pages 222-236 Equivalence Checking of Non-flat Systems Is EXPTIME-Hard....Pages 237-250 Model Checking a Path....Pages 251-265 Multi-valued Model Checking via Classical Model Checking....Pages 266-280 An Extension of Pushdown System and Its Model Checking Method....Pages 281-295 Netcharts: Bridging the Gap between HMSCs and Executable Specifications....Pages 296-310 High-Level Message Sequence Charts and Projections....Pages 311-326 Composition of Cryptographic Protocols in a Probabilistic Polynomial-Time Process Calculus....Pages 327-349 Unifying Simulatability Definitions in Cryptographic Systems under Different Timing Assumptions....Pages 350-365 Contract Signing, Optimism, and Advantage....Pages 366-382 Full Abstraction for HOPLA....Pages 383-398 Modeling Consensus in a Process Calculus....Pages 399-414 Linear Forwarders....Pages 415-430 Abstract Patterns of Compositional Reasoning....Pages 431-445 Relating Fairness and Timing in Process Algebras....Pages 446-460 A Compositional Semantic Theory for Synchronous Component-Based Design....Pages 461-476 Conditional Expectation and the Approximation of Labelled Markov Processes....Pages 477-491 Comparative Branching-Time Semantics for Markov Chains....Pages 492-507 Quantitative Relations and Approximate Process Equivalences....Pages 508-522 Back Matter....Pages -