The analysis of concurrent systems. Cambridge, September 12-16, 1983. Proceedings (Q1067764)

The book differs considerably from other Conference Proceedings. It consists of three parts, four tutorial papers concerning respectively: the Edingurgh oriented algebraic approach to concurrency (by R. Milner), Petri Nets (P. S. Thiagarajan), Temporal Logic (R. L. Schwartz, P. M. Melliar-Smith) and the use of sequential tools to analyse concurrent systems (J. R. Abrial); ten problems concerning the specification of non- sequential systems; and solutions to eight first problems (no solutions are provided to the last two ones). The problems being abstractions of real synchronisation problems are the following: (1) Two-way Channel with Disconnect, (2) Simple Network Service, (3) Synchronising Firing Squad, (4) Railway System, (5) Array Processor, (6) Packet Network with Re- routing, (7) Parallel Combinator Reduction Machine, (8) Mixing Synchronous and Asynchronous Input, and (9) ''Cash Point'' Servie, (10) m by n Matrix Switch. The solutions use various techniques, from well-known to the new ones. Temporal logic based techniques are used by H. Barringer and R. Kuiper to solve problems 1 and 6, by R. Koymans and W. P. de Roever to solve problems 1, 6 and 8, by L. Lamport to solve problems 1 and 2, by B. Moszkowski to solve problems 1, 4, 5, 6 and 8, and by J. C. Fernandez, J. P. Schwartz and J. Sifakis to specify the solution to the problem 1. The CCS and related techniques are used by J. R. Kenneway and M. R. Sleep to solve the problem 7, by R. Milner to solve the problem 3 and by M. Shields to solve the problem 4. The COSY path expression approach is used by J. Y. Cotronis and P. E. Lauer to solve the problem 1, and by P. E. Lauer to solve the problem 4. A. Kaldewaij uses the theory of traces to solve the problem 1, and C. Morgan uses so-called Z technique to the problem 2. The CSP is used by C. Morgan and C. A. R. Hoare to the problem 2 and by A. W. Roscoe to the problem 4. A. Pnueli provides a solution to the problem 2 introducing a model based on both CSP/CCS and temporal logic. P. Mosses develops a new technique solving the problem 7, and E. Astesiano and G. Reggio present also a new technique, called SMoLCs methodology, to solve the problem 3.