Rance Cleaveland (auth.), Jos C. M. Baeten, Sjouke Mauw (eds.)3540664254, 9783540664253
The 32 revised full papers presented together with four invited contributions were selected from a total of 91 submissions. The papers address all areas of semantics, logics, and verification techniques for concurrent systems, in particular process algebras, Petri nets, event-structures, real-time systems, hybrid systems, stochastic systems, decidability, model-checking, verification, refinement, term and graph rewriting, distributed programming, logic constraint programming, typing systems, etc.
Table of contents :
Temporal Process Logic….Pages 1-1
An Unfolding Algorithm for Synchronous Products of Transition Systems….Pages 2-20
Petri Nets, Configuration Structures and Higher Dimensional Automata….Pages 21-27
Expressiveness and Distributed Implementation of Concurrent Calculi with Link Mobility….Pages 28-29
Techniques for Decidability and Undecidability of Bisimilarity….Pages 30-45
Testing Concurrent Systems: A Formal Approach….Pages 46-65
Computing Minimum and Maximum Reachability Times in Probabilistic Systems….Pages 66-81
Automating Modular Verification….Pages 82-97
“Next” Heuristic for On-the-Fly Model Checking….Pages 98-113
Model Checking of Message Sequence Charts….Pages 114-129
Synthesis of Large Concurrent Programs via Pairwise Composition….Pages 130-145
Approximative Symbolic Model Checking of Continuous-Time Markov Chains….Pages 146-161
From Synchrony to Asynchrony….Pages 162-177
Reachability Analysis of (Timed) Petri Nets Using Real Arithmetic….Pages 178-193
Weak and Strong Composition of High-Level Petri Nets….Pages 194-209
Model Checking of Time Petri Nets Based on Partial Order Semantics….Pages 210-225
Generic Process Algebras for Asynchronous Communication….Pages 226-241
Timed Automata and the Theory of Real Numbers….Pages 242-257
Metrics for Labeled Markov Systems….Pages 258-273
The Expressive Power of Temporal Logic of Actions….Pages 274-286
Object Types against Races….Pages 288-303
Open Bisimulations on Chi Processes….Pages 304-319
Rectangular Hybrid Games….Pages 320-335
Localizability of Fairness Constraints and their Distributed Implementations….Pages 336-353
Generating Type Systems for Process Graphs….Pages 354-367
Weak Bisimilarity with Infinite-State Systems Can Be Decided in Polynomial Time….Pages 368-382
Robust Satisfaction….Pages 383-398
Statecharts via Process Algebra….Pages 399-414
A Partial Order Event Model for Concurrent Objects….Pages 415-430
Partial Order Reduction for Model Checking of Timed Automata….Pages 431-446
On the Semantics of Place/Transition Nets….Pages 447-462
Validating Firewalls in Mobile Ambients….Pages 463-477
On Coherence Properties in Term Rewriting Models of Concurrency….Pages 478-493
Synchronous Structures….Pages 494-508
Weakest-Congruence Results for Livelock-Preserving Equivalences….Pages 510-524
Proof-Checking Protocols Using Bisimulations….Pages 525-540
Event Structures as Presheaves—Two Representation Theorems….Pages 541-556
Subtyping and Locality in Distributed Higher Order Processes….Pages 557-572
Reviews
There are no reviews yet.