CONCUR 2007 - Concurrency Theory: 18th International Conference, CONCUR 2007, Lisbon, Portugal, September 3-8, 2007, Proceedings (Lecture Notes in Computer Science, 4703)

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. Title Page Preface Organization Table of Contents Mapping the Security Landscape: A Role for Language Techniques The Saga of the Axiomatization of Parallel Composition The Problem and Its History Background Classic Results on Equational Axiomatizations The Role of Hennessy’s Merge The Influence of Time References Rule-Based Modelling of Cellular Signalling Background A Futile Cycle Agents and Rules The Contact Map Stochastic Simulation Precedence and Stories Inhibition and Activation The EGFR Model EGFR Model Elements Ras Activation SoS Deactivation Conclusions References Appendix $\ka$, Briefly The Rule Set of the EGFR Model Making Random Choices Invisible to the Scheduler Introduction Related Work Preliminaries Simple Probabilistic Automata CCS with Internal Probabilistic Choice A Variant of CCS with Explicit Scheduler Syntax Semantics Deterministic Labelings Expressiveness of the Syntactic Scheduler Using Non-linear Labelings Testing Relations for \ccss{} Processes An Application to Security Encoding Secret Value Passing Dining Cryptographers with Probabilistic Master Dining Cryptographers with Nondeterministic Master Conclusion and Future Work References Strategy Logic Introduction GraphGames Strategy Logic Simple One-Alternation Fragment of Strategy Logic Expressive Power of Strategy Logic Model Checking Strategy Logic References Solving Games Via Three-Valued Abstraction Refinement Introduction Preliminary Definitions Game Objectives Strategies andWinning States Game Abstractions Controllable Predecessor Operators $\μ$-Calculus Reachability and Safety Games Reachability Games Safety Games Termination Approximate Abstraction Refinement Schemes Comparision with Counterexample-Guided Control Symbolic Implementation Symbolic Game Structures Symbolic Abstractions Symbolic Abstraction Refinement Abstraction Refinement for Parity Games Conclusion and Future Work References Linear Time Logics Around PSL: Complexity,Expressiveness, and a Little Bit of Succinctness Introduction Preliminaries Expressive Power and Succinctness The Complexity of \SERETL and Its Fragments Summary and Conclusion References On Modal Refinement and Consistency Background and Overview Modal Transition Systems Non-thoroughness of Modal Refinement A Thorough Refinement Is Co-NP Hard Syntactic Consistency and Syntactic Refinement Strong Modal Refinement and Strong Consistency Weak Refinement and Weak Consistency May-Weak Modal Refinement and Its Consistency Conclusion and Open Problems References Equivalence Checking for Infinite Systems Using Parameterized Boolean Equation Systems Introduction Preliminaries Bisimulation Equivalences Parameterized Boolean Equation Systems Translation for Branching Bisimulation Correctness of Transformation Example: Unbounded Queues Transformation for Other Equivalences Conclusion References Decidability Results for Well-Structured Transition Systems with Auxiliary Storage Introduction Related Work Preliminaries Well-Structured Transition Systems with Auxiliary Storage Pointed Data Structures {\wqo} Automata Decidability of the Coverability Problem Rank $k$-Approximations Effective {\wqo Automata} and Coverability Applications Multi-set Pushdown System Timed Multi-set Pushdown System Conclusions and Future Work References A Nice Labelling for Tree-Like Event Structures of Degree Introduction Event Structures and the Nice Labelling Problem Cycles and Antichains An Optimal Nice Labelling for Trees and Forests More Upper Bounds References Causal Message Sequence Charts Introduction MSCs, Causal MSCs and Causal HMSCs Regularity and Model-Checking for Causal HMSCs Semantics for Causal HMSCs Regular Sets of Linearizations Inclusion and Intersection Non-emptiness of Causal HMSCs Window-Bounded Causal HMSCs Relationship with Other Scenario Models Conclusion References Checking Coverage for Infinite Collections of Timed Scenarios Introduction Preliminaries on MSCs Message Sequence Charts Message Sequence Graphs Adding Time to Scenarios Time-Constrained MSCs Timed MSCs Time-Constrained MSGs Timed Message-Passing Automata The Coverage Problem Coverage for Locally Synchronized TC-MSGs Discussion References Is Observational Congruence Axiomatisable in Equational Horn Logic? Introduction The Process Language $\bccspp$ A Pure Horn Axiomatisation Can Horn Eliminate Unguardedness? Discussion, Conclusions and Future Work References The $\Must$ Preorder Revisited An Algebraic Theory for Web Services Contracts Introduction The Contract Language The Subcontract Relation Dual Contracts Choreographies Concluding Remarks References Topology-Dependent Abstractions of Broadcast Networks Introduction bKlaim Syntax Operational Semantics Abstract Transition Systems Exposed Actions Abstract Transition Systems Interpretation of ACTL Properties Constructing Abstract Transition Systems Transfer Functions Worklist Algorithm Conclusion References On the Expressive Power of Global and Local Priority in Process Calculi Introduction Contribution of This Paper Structure of the Paper Calculi The $\pi$-Calculus The$\ bpi$-Calculus The CPG Language The FAP Language Encodings The Leader Election Problem The Last Man Standing Problem Separation Results Leader-Election-Based Separation Results LMS-Based Separation Results Conclusion References A Marriage of Rely/Guarantee and Separation Logic Introduction Technical Background Local Reasoning – Separation Logic The Combined Logic Describing Interference Stability Local and Shared State Assertions Ownership Transfer Specifications and Proof Rules Example Semantics and Soundness Related Work Conclusion References Fair Cooperative Multithreading Introduction Syntax OperationalSemantics The Type and Effect System The Termination Property Conclusion References Precise Fixpoint-Based Analysis of Programs with Thread-Creation and Procedures Introduction Parallel Flow Graphs Dataflow Analysis ForwardAnalysis Backward Analysis Possible Interference Parallel Calls Conclusion References Automatic Derivation of Compositional Rules in Automated Compositional Reasoning Introduction Preliminaries Classical Interpretation Limitation of Classical Interpretation Interpretation \`a la Abadi and Plotkin Applications On Invertibility Conclusions References Compositional Event Structure Semantics for the Internal $\pi$-Calculus Introduction Internal $\pi$-Calculus Event Structures The Parallel Composition Event Structure Semantics Generalised Relabelling Definition of the Semantics Examples Properties of the Semantics Asynchronous $\pi$I-Calculus Denotational Semantics Properties of the Semantics Related and Future Work References A Substitution of Sequences Interpreting a Finitary Pi-calculus in Differential Interaction Nets Introduction Differential Interaction Nets Presentation of the Cells Reduction Rules Defining the Reduction Confluence A Transition System of Simple Nets A Toolbox for Process Calculi Interpretation Compound Cells Communication Tools Useful Reductions A Polyadic Finitary $\pi$-calculus and Its Encoding An Execution Model Translation of Processes Comparing the Transition Systems References Mobility Control Via Passports Introduction Typed DÏ€ with Passports Loyal Observational Equivalence Loyal Bisimilarity Conclusion and Perspectives References Reduction Semantics Coalgebraic Models for Reactive Systems Introduction The Theory of Reactive Systems Coalgebras and Structured Coalgebras Coalgebraic Models of $\CTSs$ Coalgebraic Models of $\ITSs$ Normalized Coalgebras Isomorphism Theorem From \ilts\ to $\sim_{SAT}$ ThroughNormalization Conclusions References Reactive Systems over Directed Bigraphs Introduction Directed Bigraphs Directed Bigraphical Reactive and Transition Systems Directed Bigraphical Reactive Systems Directed Bigraphical Transition Systems Reducing Directed Bigraphical Transition Systems Engaged Transition System Definite Engaged Transition System Extending to Non-hard Abstract Bigraphs An Application: The Fusion Calculus Conclusions References Asynchronous Games: Innocence Without Alternation Introduction The Cube Property Positionality in Asynchronous Games Ingenuous Strategies in Asynchronous Games Ingenuous Strategies in Concurrent Games Innocent Strategies References Bisimulation and Logical Preservation for Continuous-Time Markov Decision Processes Introduction Continuous-Time Markov Decision Processes The Probability Space The Probability Measure Strong Bisimulation Continuous Stochastic Logic Syntax and Semantics Strong Bisimilarity Preserves CSL Conclusion References Strategy Synthesis for Markov Decision Processes and Branching-Time Logics Introduction Basic Definitions Markov Chains The Logic qPECTL$^*$ Games and Strategies The Synthesis Problem for detPECTL$^*$ The Synthesis Problem for qPECTL$^*$ and Finite-Memory Strategies qPCTL and Finite-Memory Strategies References Timed Concurrent Game Structures Introduction Definitions Untimed Concurrent Game Structures Timed Concurrent Game Structures Region Equivalence and Strategies Region Equivalence Simplifying Strategies RegionCGS TimedATL Model-Checking Ruling Out Zeno Strategies Conclusion and Perspectives References Pushdown Module Checking with Imperfect Information Introduction Preliminaries Imperfect Information Pushdown Module Checking Module Checking with Visible Pushdown Store Discussion References Alternating Automata and a Temporal Fixpoint Calculus for Visibly Pushdown Languages Introduction Preliminaries Alternating Visibly Pushdown Automata Alternating Jump Finite-State Automata Relation Between Nondeterministic Visibly Pushdown Automata and $\AJA$ Decision Problems for Alternating Jump Automata Conclusion References Visibly Pushdown Linear-Time $\mu$-Calculus (\VPMU Temporal Antecedent Failure: Refining Vacuity Introduction Preliminaries Notations Temporal Logic Regular Expressions Positions in Regular Expressions and Related Partial Orders Temporal Antecedent Failure (TAF) and Its Reasons Temporal Antecedent Failure Moving to Regular Expressions Defining TAF Reasons Implementation Detecting Antecedent Failure and Its Reasons Witness Generation Procedure for Detecting TAF, Its Reasons and GeneratingWitnesses Discussion References Author Index This volume contains the proceedings of the 18th International Conference on Concurrency Theory, held at the Gulbenkian Foundation, Lisbon, Portugal, September 3-8, 2007. Since its?rst edition back in 1990, Concur has been a leading conference in concurrency theory, attracting researchers, graduate s- dents, and practitioners, to exchange ideas, progresses, and challenges. TheConcurconferencehastraditionallycoveredalargespectrumofthe?eld, including invited lecturers and tutorials by prominent researchers, contributed technical papers, and several associated workshops. Main topics include basic models and logics of concurrent and distributed computation (such as process algebras, Petri nets, domain theoretic or game theoretic models, modal and temporal logics), specialized models or classes of systems (such as synchronous systems, real time and hybrid systems, stochastic systems, databases, mobile and migrating systems, protocols, biologically inspired systems), related ver- cation techniques and tools (including state-space exploration, model-checking, synthesis, abstraction, automated deduction, testing), and concurrent progr- ming (such as distributed, constraint or object-oriented, graphrewriting, as well as associated type systems, static analyses, and abstract machines). This year, the Program Committee, after a careful and thorough reviewing process, selected for inclusion in the programme 30 papers out of 112 subm- sions. Eachsubmissionwasevaluatedbyatleastthreereferees, andtheaccepted papers were selected during a one-and-a-half-week electronic discussion. The volume opens with the invited contributions by Luca Aceto (Reykjavþ?k), Vincent Danos (Paris 7), and Fred B. Schneider (Cornell). The program also included an additional invited lecture by Peter O'Hearn (QMU London) and an additional tutorial by Josþ e Luiz Fiadeiro (Leicester), all of which, we believe, complimented the technical papers rather well This book constitutes the refereed proceedings of the 17th International Conference on Concurrency Theory, CONCUR 2007, held in Lisbon, Portugal, September 3-8, 2007. The 30 revised full papers presented together with 3 invited papers were carefully reviewed and selected from 112 submissions. The topics include model checking, process calculi, minimization and equivalence checking, types, semantics, probability, bisimulation and simulation, real time, and formal languages