CONCUR 2000 - Concurrency Theory: 11th International Conference, University Park, PA, USA, August 22-25, 2000 ProceedingsCatuscia Palamidessi This volume contains the proceedings of the 11th International Conference on Concurrency Theory (CONCUR 2000) held in State College, Pennsylvania, USA, during 22-25 August 2000. 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 - plications, and of the scienti?c relevance of their foundations. The scope covers all areas of semantics, logics, and veri?cation techniques for concurrent systems. Topics include concurrency related aspects of: models of computation, semantic domains, process algebras, Petri nets, event structures, real-time systems, hybrid systems, decidability, model-checking, veri?cation techniques, re?nement te- niques, term and graph rewriting, distributed programming, logic constraint p- gramming, object-oriented programming, typing systems and algorithms, case studies, tools, and environments for programming and veri?cation. The ?rst two CONCUR conferences were held in Amsterdam (NL) in 1990 and 1991. The following ones in Stony Brook (USA), Hildesheim (D), Uppsala (S), Philadelphia (USA), Pisa (I), Warsaw (PL), Nice (F), and Eindhoven (NL). The proceedings have appeared in Springer LNCS, as Volumes 458, 527, 630, 715, 836, 962, 1119, 1243, 1466, and 1664. |
Contents
Combining Theorem Proving and Model Checking through Symbolic Analysis | 1 |
Verification Is Experimentation | 17 |
Compositional Performance Analysis Using Probabilistic IO Automata | 25 |
Formal Models for CommunicationBased Design | 29 |
The KLAIM Experience | 48 |
Exploiting Hierarchical Structure for Efficient Formal Verification | 66 |
From Process Calculi to Process Frameworks | 69 |
Verification Using Tabled Logic Programming | 89 |
A Theory of Testing for Markovian Processes | 305 |
Reasoning about Probabilistic Lossy Channel Systems | 320 |
Weak Bisimulation for Probabilistic Systems | 334 |
Obeying the Laws | 350 |
Secrecy and Group Creation | 365 |
On the Reachability Problem in Cryptographic Protocols | 380 |
Secure Information Flow for Concurrent Processes | 395 |
LP Deadlock Checking Using Partial Order Dependencies | 410 |
Control and Synthesis | 92 |
Model Checking with Finite Complete Prefixes Is PSPACEComplete | 108 |
Verifying Quantitative Properties of Continuous Probabilistic Timed Automata | 123 |
The Impressive Power of Stopwatches | 138 |
Optimizing Büchi Automata | 153 |
Reasoning about Partial State Spaces | 168 |
Reachability Analysis for Some Models of InfiniteState Transition Systems | 183 |
Process Spaces | 199 |
Failure Semantics for the Exchange of Information in MultiAgent Systems | 214 |
ProofOutlines for Threads in Java | 229 |
Deriving Bisimulation Congruences for Reactive Systems | 243 |
Bisimilarity Congruences for Open Terms and Term Graphs via Tile Logic | 259 |
Process Languages for Rooted Eager Bisimulation | 275 |
Action Contraction | 290 |
Pomsets for Local Trace Languages Recognizability Logic Petri Nets | 426 |
Functional Concurrent Semantics for Petri Nets with Read and Inhibitor Arcs | 442 |
The Control of Synchronous Systems | 458 |
Typing Nonuniform Concurrent Objects | 474 |
An ImplicitlyTyped DeadlockFree Process Calculus | 489 |
Typed Mobile Objects | 504 |
Synthesizing Distributed FiniteState Systems from MSCs | 521 |
Emptiness Is Decidable for Asynchronous Cellular Machines | 536 |
Revisiting Safety and Liveness in the Context of Failures | 552 |
WellAbstracted Transition Systems Extended Abstract | 566 |
A Unifying Approach to DataIndependence | 581 |
Chi Calculus with Mismatch | 596 |
Author Index | 611 |
Other editions - View all
CONCUR 2000 - Concurrency Theory: 11th International Conference, University ... Catuscia Palamidessi No preview available - 2000 |
CONCUR 2000 - Concurrency Theory: 11th International Conference, University ... Catuscia Palamidessi No preview available - 2014 |
Common terms and phrases
abstract action agent algebra algorithm ambient arity atomic automata automaton behavior bisimilarity bisimulation Büchi automata calculus channel communication Computer Science concurrent configuration congruence consider constraints construct context corresponding counter defined Definition denote domain dynamically typed environment equivalence example execution extended FIFO formal formula fusion given graph i-net infinite input Kripke structure labelled transition labelled transition system Lecture Notes Lemma linear LNCS Markovian method model checking module node nondeterministic Notes in Computer notion object operational semantics operator output Petri net pomsets prefix preorder problem Proc process calculus programming proof Proposition protocol PSPACE PSPACE-complete Pure(P reachability reduction restriction rules satisfies semantics sequence simulation specification Springer-Verlag symbolic synchronous T₁ temporal logic Theorem tile trace language transition relation transition system tuple tuple space type system variables verification weak bisimulation