Colin Stirling (auth.), Insup Lee, Scott A. Smolka (eds.)3540602186, 9783540602187
The volume presents seven invited contributions by outstanding researchers and 33 refereed full research papers selected by the program committee out of a total of 91 submissions. The collection of articles gives a representative overview on what happened in this area of research, since the last CONCUR conference took place. There are sections on model checking, mobile processes, process theory, true concurrency, process algebra, probabilistic automata, real-time systems, testing semantics, decidability results, refinement theory, and linear-time logics.
Table of contents :
Local model checking games (extended abstract)….Pages 1-11
Compositional proof systems for model checking infinite state processes….Pages 12-26
Compositional model checking of real time systems….Pages 27-41
Checking bisimilarity for finitary π-calculus….Pages 42-56
The weak late π-calculus semantics as observation equivalence….Pages 57-71
The fixpoint-analysis machine….Pages 72-87
Unique fixpoint induction for mobile processes….Pages 88-102
A polymorphic type system for the polyadic π-calculus….Pages 103-116
Fibrational control structures….Pages 117-129
Fully abstract models for nondeterministic regular expressions….Pages 130-144
A Petri net semantics for π-calculus….Pages 145-159
A complete theory of deterministic event structures….Pages 160-174
Characterizing behavioural congruences for Petri nets….Pages 175-189
Verification of a distributed summation algorithm….Pages 190-203
Confluence for process verification….Pages 204-218
Axiomatisations of weak equivalences for De Simone languages….Pages 219-233
A compositional trace-based semantics for probabilistic automata….Pages 234-248
Acceptance trees for probabilistic processes….Pages 249-263
Will I be pretty, will I be rich? Some thoughts on theory vs. practice in systems engineering….Pages 264-268
Towards a denotational semantics for ET-LOTOS….Pages 269-283
Reachability analysis at procedure level through timing coincidence….Pages 284-298
Faster asynchronous systems….Pages 299-312
Fair testing….Pages 313-327
Formal methods technology transfer: Impediments and innovation (abstract)….Pages 328-332
Decidability of simulation and bisimulation between lossy channel systems and finite state systems….Pages 333-347
Checking regular properties of Petri nets….Pages 348-362
Metric predicate transformers: Towards a notion of refinement for concurrency….Pages 363-377
A refinement theory that supports both ’decrease of nondeterminism’ and ’increase of parallelism’….Pages 378-392
Model checking and efficient automation of temporal reasoning….Pages 393-394
Verifying parameterized networks using abstraction and regular languages….Pages 395-407
On the complexity of branching modular model checking….Pages 408-422
Axiomatising linear time mu-calculus….Pages 423-437
A trace consistent subset of PTL….Pages 438-452
Tutorial: Proving properties of concurrent systems with SPIN….Pages 453-455
On sharing and determinacy in concurrent systems….Pages 456-470
Process semantics of graph reduction….Pages 471-485
Bisimulations for a calculus of broadcasting systems….Pages 486-500
Delayed choice for process algebra with abstraction….Pages 501-515
CTR: A calculus of timed refinement….Pages 516-530
Temporal logic + timed automata: Expressiveness and decidability….Pages 531-545
Reviews
There are no reviews yet.