This book contains a selection of research papers describingrecent advancesin the theory of concurrent systems andtheir applications. The papers were all presented at theCONCUR '92 conference, which has emerged as the premiereconference on formal aspects of concurrency. The authorsinclude such prominent researchers as R. Milner, A. Pnueli,N. Lynch, and V.R. Pratt. The results represent advances inthe mathematical understanding of the behavior of concurrentsystems: topics covered include process algebras, models oftrue concurrency, compositional verification techniques,temporal logic, verification case studies, models ofprobabilistic and real-time systems, models of systems withdynamic structure, and algorithms and decidability resultsfor system analysis.A key feature of CONCUR is its breadth: in one volume itpresents a snapshot of the state of the art in concurrencytheory. Assuch, it is indispensible to researchers - andwould-be researchers - in theformal analysis of concurrentsystems.
The polyadic ?-calculus.- Testing equivalence for mobile processes.- Testing equivalence for Petri Nets with action refinement: Preliminary report.- The problem of "weak bisimulation up to".- On the uniqueness of fixpoints modulo observation congruence.- Verification of parallel systems via decomposition.- Interface refinement in reactive systems.- Concurrent testing of processes.- A theory of processes with localities.- Model checking for context-free processes.- Bisimulation equivalence is decidable for all context-free processes.- Distributed bisimularity is decidable for a class of infinite state-space systems.- How vital is liveness? Verifying timing properties of reactive and hybrid systems.- Preserving specific properties in program development.- Sometimes 'some' is as good as 'all'.- The weakest compositional semantic equivalence preserving nexttime-less linear temporal logic.- Propositional temporal logics and equivalences.- The duality of time and information.- Homology of higher dimensional automata.- Posets for configurations!.- On the semantics of Petri Nets.- Structural operational specifications and trace automata.- At-most-once message delivery A case study in algorithm verification.- Games I/O automata play.- Minimization of timed transition systems.- Using CSP to verify a timed protocol over a fair medium.- Timed Ethernet: Real-time formal specification of Ethernet.- Implementing LOTOS specifications by communicating state machines.- Discrete time process algebra.- The silent step in time.- Action transducers and timed automata.- Compositional verification of probabilistic processes.- Axiomatizing probabilistic processes: ACP with generative probabilities.- Embeddings among concurrent programming languages.- Logic of trace languages.- Multiway synchronization verified with coupled simulation.- Programming in a general model of synchronization.- Operational and compositional semantics of synchronous automaton compositions.- Towards a theory of actor computation.