From: sas@sbcs.sunysb.edu
Newsgroups: news.announce.conferences
Subject: CONCUR '92 --- Abstracts of Invited Talks & Tutorials
Date: 28 Jul 92 00:02:13 GMT
Expires: Thu, 27 Aug 1992 07:00:00 GMT
Organization: (none)


Below, please find the abstracts of the inivted talks and tutorials to be given
at CONCUR '92, Third Int'l Conf. on Concurrency Theory, 24-27 Aug. 1992, Stony
Brook, NY.  A LaTex file of the final program and Call for Registration is
available via anonymous ftp from sbcs.sunysb.edu (130.245.1.15).  The file is
located in pub/CONCUR92/cfr.tex.Z and is in compressed format.
----------

		       ABSTRACTS OF INVITED TALKS

			       CONCUR '92


 .----------------------------------------------------------------------------.
 |                                                                            |
 |                        Discrete Time Process Algebra                       |
 |                                                                            |
 |                                 Jos Baeten                                 |
 |                     Eindhoven University of Technology                     |
 |                                                                            |
 | Process Algebra in the form of ACP, CCS or CSP describes the main features |
 | of imperative concurrent programming without any explicit mention of       |
 | time.  Implicitly, time is present in the interpretation of sequential     |
 | composition, in that the first of a sequenced pair of processes must be    |
 | executed before the second.  It may be felt as a weakness that time only   |
 | features implicitly.  Indeed a quantitative view on the relationship       |
 | between process execution and progress of time is definitely absent in     |
 | these calculi.  This seems worse than it actually is.  Nothing prevents    |
 | one to introduce timer processes that represent clocks, to have processes  |
 | interacting with these clocks and to have synchronisations between the     |
 | clocks in ACP, CCS or CSP.                                                 |
 |                                                                            |
 | Of course timing aspects can be described more uniformly if process        |
 | algebras are given that provide standardised features to incorporate a     |
 | quantitative view on time.  Obvious as this may seem, the more obvious     |
 | observation is that in a few years so many different formats for timed     |
 | process algebras have been introduced that this uniformity seems to be     |
 | further away than before.  There are several reasons for the emerging      |
 | spectrum of timed process algebras.  This can be explained by considering  |
 | various options for adding time.  The most obvious option is to represent  |
 | time by means of non-negative reals, and to have time stamps on actions.   |
 |                                                                            |
 | Another options is to divide time in slices indexed by natural numbers, to |
 | have a time stamping mechanism that provides each action with the time     |
 | slice in which it occurs and to have a time order within each slice only.  |
 | This has been worked out in ATP, a process algebra that adds time slicing  |
 | to aprACP, a version of ACP based on action prefixing rather than          |
 | sequential composition.                                                    |
 |                                                                            |
 | In this talk we extend ACP to a discrete time process algebra.  This is    |
 | done by adding a new process constructor which represents the delay of a   |
 | process for one time unit. For practical applications, we include further  |
 | the key operators of ATP, namely unit delay and maximal progress           |
 | composition.  We design our discrete time process algebra in an            |
 | incremental way, and motivate our choices with each increment of the       |
 | algebra and compare it with other developments of discrete time process    |
 | algebra.                                                                   |
 |                                                                            |
 `----------------------------------------------------------------------------'

 .----------------------------------------------------------------------------.
 |                                                                            |
 |                       At-Most-Once Message Delivery:                       |
 |                   A Case Study in Algorithm Verification                   |
 |                                                                            |
 |                                 Nancy Lynch                                |
 |                                     MIT                                    |
 |                                                                            |
 | The at-most-once message delivery problem involves delivering a sequence   |
 | of messages submitted by a user at one location to another user at another |
 | location.  If no failures occur, all messages should be delivered in the   |
 | order in which they are submitted, each exactly once.  If failures (in     |
 | particular, node crashes, lost messages or timing anomalies) occur, some   |
 | messages might be lost, but the remaining messages should not be reordered |
 | or duplicated.                                                             |
 |                                                                            |
 | This talk examines two of the best-known algorithms for solving this       |
 | problem: the clock-based protocol of [LSW] and the five-packet interchange |
 | protocol of [B]] It is shown that both of these protocols can be           |
 | understood as implementations of a common (untimed) protocol that we call  |
 | the generic protocol.  It is also shown that the generic protocol meets    |
 | the problem specification.                                                 |
 |                                                                            |
 | The development is carried out in the context of (timed and untimed)       |
 | automata [LV], [LT], using simulation techniques [LV].  It exercises many  |
 | aspects of the relevant theory, including timed and untimed automata,      |
 | refinement mappings, forward and backward simulations, history and         |
 | prophecy variables.  The theory provides insight into the algorithms, and  |
 | vice versa.                                                                |
 |                                                                            |
 | This talk represents joint work with Butler Lampson and Jorgen             |
 | Sogaard-Andersen.                                                          |
 |                                                                            |
 | [LSW] Barbara Liskov, Luiba Shrira and John Wroclawski, "Efficient         |
 |       At-Most-Once Messages Based on Synchronized Clocks."                 |
 |       MIT/LCS/TR-476, April, 1990, Laboratory for Computer Science,        |
 |       Massachusetts Institute of Technology, Cambridge, MA 02139.          |
 |                                                                            |
 |   [B] Dag Belsnes, "Single Message Communication."  IEEE                   |
 |       Transactions on Communications, Vol. Com-24, No. 2, February,        |
 |       1976.                                                                |
 |                                                                            |
 |  [LV] Nancy Lynch and Frits Vaandrager, "Forward and Backward              |
 |       Simulations for Timing-Based Systems."  In Proceedings of REX        |
 |       Workshop "Real-Time:  Theory in Practice," Springer-Verlag,          |
 |       LNCS 600, 1992, Mook, The Netherland.                                |
 |                                                                            |
 |  [LT] Lynch, N. and Tuttle, M. "An Introduction to Input/Output            |
 |       Automata," CWI-Quarterly, No. 3, Vol. 2, September, 1989,            |
 |       pages 219-246.                                                       |
 |                                                                            |
 `----------------------------------------------------------------------------'

 .----------------------------------------------------------------------------.
 |                                                                            |
 |                          The Polyadic pi Calculus                          |
 |                                                                            |
 |                                Robin Milner                                |
 |                           University of Edinburgh                          |
 |                                                                            |
 | The pi calculus is a calculus of concurrent processes based upon the idea  |
 | of naming.  It models dynamically changing concurrent systems, has a rich  |
 | algebraic theory, and contains in a precise way both functions (the lambda |
 | calculus) and data structures, represented as processes.  The calculus is  |
 | a generalization of CCS, and was introduced by Robin Milner, Joachim       |
 | Parrow and David Walker, based on important ideas of Mogens Nielsen and    |
 | Uffe Engberg.                                                              |
 |                                                                            |
 | The way in which everything is built upon naming is this: When two         |
 | processes interact, they use a name (which can be thought of as a          |
 | channel).  This name is called the subject of the interaction.  The object |
 | of an interaction (its information content) is also a name; this is the    |
 | mention of a name, not the use of it.  To receive a name is to acquire the |
 | ability to use it, perhaps to interact with a process which was previously |
 | inaccessible. This process may indeed represent a datum, as explained      |
 | above;  then one can think of the datum itself having been received.       |
 |                                                                            |
 | In this lecture I shall discuss the polyadic version of the pi calculus,   |
 | which supports a very fruitful notion of sort and sorting, akin to simple  |
 | typing in the lambda calculus. It will be seen how different sortings are  |
 | appropriate for different applications.  The encoding of the lambda        |
 | calculus into pi calculus, and the uniform representation of data          |
 | structures, are best seen in the polyadic setting with suitable sortings.  |
 |                                                                            |
 `----------------------------------------------------------------------------'

 .----------------------------------------------------------------------------.
 |                                                                            |
 |                            How Vital is Liveness?                          |
 | 		Proving Timing Properties of Hybrid and Reactive Systems      |
 |                                                                            |
 |                                Amir Pneuli                                 |
 |                       Weizmann Institute of Science                        |
 |                                                                            |
 | We propose a framework for the formal specification and verification of    |
 | timed and hybrid systems.  For timed systems we propose a specification    |
 | language that refers to time only through age functions which measure the  |
 | length of the most recent time interval in which a given formula has been  |
 | continuously true.                                                         |
 |                                                                            |
 | We then consider hybrid systems, which are systems consisting of a         |
 | nontrivial mixture of discrete and continuous components, such as a        |
 | digital controller that controls a continuous environment.  The proposed   |
 | framework extends the temporal logic approach which has proven useful for  |
 | the formal analysis of discrete systems such as reactive programs.  The    |
 | new framework consists of a semantic model for hybrid time, the notion of  |
 | phase transition systems, which extends the formalism of discrete          |
 | transition systems, an extended version of Statecharts for the             |
 | specification of hybrid behaviours, and an extended version of temporal    |
 | logic that enables reasoning about continuous change.                      |
 |                                                                            |
 | The talk is based on extensive collaboration with Z. Manna, T. Henzinger,  |
 | O. Maller and Y. Kesten.                                                   |
 |                                                                            |
 |                                                                            |
 `----------------------------------------------------------------------------'

 .----------------------------------------------------------------------------.
 |                                                                            |
 |                     The Duality of Time and Information                    |
 |                                                                            |
 |                                Vaughan Pratt                               |
 |                             Stanford University                            |
 |                                                                            |
 | The states of a computing system bear information and change time, while   |
 | its events bear time and change information.  We develop a primitive       |
 | algebraic model of this duality of time and information for straightline   |
 | code in the absence of nondeterminism and concurrency, where time and      |
 | information are linearly ordered, demonstrating that this natural duality  |
 | of computation is more fundamental than the natural logic of computation   |
 | in which nondeterminism is disjunction and concurrency conjunction.        |
 |                                                                            |
 | To accommodate distributed computing systems we then bring in these two    |
 | logical connectives, in the process passing to partially ordered time and  |
 | information.  Some flexibility in how this is done permits a perfectly     |
 | symmetric logic of computation.  The natural form taken by this logic is   |
 | essentially full linear logic, showing that linear logic arises            |
 | automatically as a logic of full computation, namely computation attaching |
 | equal importance to nondeterminism and concurrency.                        |
 |                                                                            |
 | We conclude with an assessment of the prospects for extending the duality  |
 | to other organizations of time and information besides partial orders in   |
 | order to accommodate real time, nonmonotonic logic, and automata that can  |
 | forget.                                                                    |
 |                                                                            |
 `----------------------------------------------------------------------------'


		       ABSTRACTS OF TUTORIALS

			       CONCUR '92


 .----------------------------------------------------------------------------.
 |                                                                            |
 |                  Finite-State Models of Real-time Behavior                 |
 |                                                                            |
 |                      Rajeev Alur           David L. Dill                   |
 |                 AT&T Bell Laboratories  Stanford University                |
 |                                                                            |
 | Finite-state models of various kinds have been very useful for automatic   |
 | formal verification of concurrent systems.  Many verification algorithms   |
 | have been developed for both branching-time and linear-time models, and    |
 | the methods have been applied successfully to non-trivial systems.         |
 |                                                                            |
 | However, there is now a great deal of interest in modelling and formal     |
 | verification of real-time concurrent systems, for which quantitative       |
 | delays are crucial to "correct" behavior.  It is not too difficult to      |
 | incorporate timing constraints into ordinary finite automata if time is    |
 | considered to be discrete.  However, time is often regarded as a           |
 | continuous quantity, and continuous time is the most natural model for     |
 | some physical processes.                                                   |
 |                                                                            |
 | One method for incorporating continuous time into finite automata is to    |
 | annotate finite-state models with real-valued counters, called clocks,     |
 | which keep track of the delays between events.  These tutorial lectures    |
 | will discuss some of the surprises that arise from the study of timed      |
 | finite automata, as well as how they can be applied to the modelling and   |
 | verification of real-time systems.                                         |
 |                                                                            |
 | In the linear-time case, we can consider these automata to accept timed    |
 | strings, which record not only the order of events but their times of      |
 | occurrence.  The set of timed strings accepted by a timed automaton can be |
 | considered to be a timed formal language, which immediately prompts one to |
 | ask the usual questions about decidability and closure properties.  Some   |
 | of the answers are surprising: for nondeterministic automata, emptiness is |
 | decidable but universality is not (while in the discrete case, both are    |
 | decidable).                                                                |
 |                                                                            |
 | In the branching-time case, it is interesting to consider the problem of   |
 | model-checking of formulas in a timed dialect of computation tree logic    |
 | (CTL).  There are some surprises here, also:  the model-checking problem   |
 | is fully decidable, but the logic itself is not.                           |
 |                                                                            |
 | We believe that timed automata in various forms will be useful for         |
 | modelling and verifying real-time systems.  Furthermore, the results can   |
 | be adapted to other similar problems (for example, checking bisimulation   |
 | in real-time process algebras).  There are also numerous questions about   |
 | timed languages and automata that have yet to be answered.                 |
 |                                                                            |
 `----------------------------------------------------------------------------'

 .----------------------------------------------------------------------------.
 |                                                                            |
 |                       Introduction to Process Algebra                      |
 |                                                                            |
 |                              Rob van Glabbeek                              |
 |                             Stanford University                            |
 |                                                                            |
 | This tutorial gives an introduction to and overview of some languages and  |
 | models for representing and reasoning about processes. Attention will be   |
 | restricted to the more classical approaches, omitting recent developments  |
 | on real-time and value passing.                                            |
 |                                                                            |
 | First of all system description languages like CCS, CSP, COSY, ACP and     |
 | MEIJE will be presented and compared. Translations from one language in    |
 | the other will be provided, and the relative expressiveness of the various |
 | languages will be analyzed. Particular attention will be paid to the       |
 | treatment of nondeterminism, communication between parallel processes,     |
 | recursion, abstraction from internal actions, successful termination,      |
 | deadlock, divergence and underspecification.                               |
 |                                                                            |
 | The semantics of the languages can be given by means of an interpretation  |
 | in a model of concurrency, or process algebra. This is usually done in two |
 | steps. In step 1 an interpretation of the language in an underlying model  |
 | (often a particular brand of process graphs, Petri nets or event           |
 | structures) is given. Then in step 2 an equivalence relation on this model |
 | is divided out in order to abstract from unwanted details in system        |
 | descriptions. Of course this equivalence should be a congruence for all    |
 | language constructs.                                                       |
 |                                                                            |
 | Usually step 1 is performed using denotational semantics: an operator is   |
 | associated with every language construct and recursion is dealt with by    |
 | means of fixed point techniques. Alternatively, in case the underlying     |
 | model is based on event structures, the syntactic tree of a process        |
 | expression (or actually the syntactic graph, after eliminating recursion   |
 | operators) can smoothly be transformed in an event structure. In case of a |
 | transition oriented underlying model (brands of process graphs or Petri    |
 | nets), step 1 can conveniently be performed by means of structured         |
 | operational semantics: the transitions in system representations are       |
 | derived step for step, using a kind of inference mechanism.                |
 |                                                                            |
 | If the underlying model is considered abstract enough for a desired        |
 | application, step 2 can be skipped. Such models are called explicit models |
 | and include the models based on non-well-founded sets or on metric spaces, |
 | projective limit models and the models in which a process is represented   |
 | by a set of executions (modelled as traces, failure pairs, partial ordered |
 | multisets, etc.).                                                          |
 |                                                                            |
 | Although many different underlying models have been proposed, there exist  |
 | canonical translations between them. Modulo these translations the models  |
 | differ only in size (it can be that a system can be represented in one     |
 | model, but not in another) and in the level of detail of process           |
 | representations (it can be that two systems are represented differently in |
 | one model, but have the same representation in another one).               |
 |                                                                            |
 | Like the underlying models, also the proposed equivalence relations to be  |
 | divided out on these models come in huge quantities.  The choice of such   |
 | an equivalence is not without consequences: they are used to determine if  |
 | one system is a correct implementation of another one.  Semantic           |
 | equivalences determine or are determined by the relevant properties of     |
 | process representations: two processes are identified iff they have the    |
 | same relevant properties. Of course it is application dependent which      |
 | properties are relevant. Therefore many semantic equivalences coexist.     |
 |                                                                            |
 `----------------------------------------------------------------------------'

 .----------------------------------------------------------------------------.
 |                                                                            |
 |                           Models for Concurrency                           |
 |                                                                            |
 |                               Mogens Nielsen                               |
 |                              Aarhus University                             |
 |                                                                            |
 | A number of formal models have been suggested and studied in the           |
 | literature as frameworks for understanding the nature of distributed       |
 | computations.  Each model has its own set of techniques for expressing and |
 | reasoning about distributed computational systems. The choice of model for |
 | a concrete application is often based on a mixture of pragmatic and formal |
 | considerations. As an aid in this process, these models are often          |
 | classified according to their expressive power, e.g interleaving versus    |
 | noninterleaving, linear time versus branching time, system versus          |
 | behavioural, etc. And recently, these kinds of classifications have been   |
 | supported by theoretical results expressing formal relationships between   |
 | models -- the topic of this talk.                                          |
 |                                                                            |
 | The models and their relationships will be expressed categorically. The    |
 | models will be equipped with a notion of "simulation" morphisms, and the   |
 | relationships will be expressed in terms of certain types of adjunctions   |
 | between our (categories of) models, based on functors viewed as            |
 | translations between individual models. Not only does this give a unified  |
 | presentation of the models (also used in this talk), and formal ways of    |
 | expressing concepts like "one model being more abstract than another"; but |
 | also it turns out that constructions used in languages like CCS and CSP,   |
 | based on synchronous communication, can be viewed as universal in these    |
 | categories, and hence the semantics may be described in a uniform way for  |
 | many different structures; and in the formal translation between models    |
 | one may use preservation properties of adjoints.                           |
 |                                                                            |
 | In this tutorial we shall                                                  |
 |                                                                            |
 |   - give a brief introduction to some fundamental models for concurrency,  |
 |     including (Asynchronous) Transition Systems, Petri Nets,               |
 |     Synchronization Trees, Event Structures, Hoare Traces and              |
 |     Mazurkiewics Traces, and their notions of "simulation" morphisms used  |
 |     in this presentation; focussing on the similarities and differences    |
 |     of the models with respect to  expressive power, based on examples;    |
 |                                                                            |
 |   - motivate and present the types of results mentioned above; focussing   |
 |     on presentation and interpretation of a formal classification of       |
 |     models in terms of adjunctions, and also illustrating operational and  |
 |     denotational semantics of process algebra in this context;             |
 |                                                                            |
 |   - present one of the adjunctions -- relationship between Transition      |
 |     Systems and Petri Nets -- in some detail; this is one example of an    |
 |     important result contributing to the understanding of the distinction  |
 |     between so-called interleaving and noninterleaving models.             |
 |                                                                            |
 | This talk is based on a chapter "Models for Concurrency" being written     |
 | jointly with Glynn Winskel for the Handbook of Logic in Computer Science   |
 | (Oxford University Press).                                                 |
 |                                                                            |
 `----------------------------------------------------------------------------'

 .----------------------------------------------------------------------------.
 |									      |
 |    Efficient Program Transformations for Resilient Parallel Computation    |
 |									      |
 |	                         Krishna Palem				      |
 |			IBM Research Center, Yorktown Heights		      |
 |                                                                            |
 | With hardware becoming cheaper, it is expected that massively parallel     |
 | systems with large numbers of processors will offer increasingly faster    |
 | computational speeds, at low cost.  Unfortunately, these massively         |
 | parallel machines tend to become increasingly fault-prone as well.  For    |
 | example, the larger the number of processors, the greater the probability  |
 | of some of them failing.  To further compound this problem, much of        |
 | program or algorithm design is typically performed in the context of an    |
 | ideal parallel machine that is unencumbered by failures or other           |
 | imperfections intrinsic to its realistic counterpart.  As a consequence,   |
 | these ideal programs are not even guaranteed to run correctly on real      |
 | implementations of parallel machines, whenever the ideal assumptions of    |
 | the programming model are not supported.  The aim of this tutorial is to   |
 | describe strategies supporting the resilient (correct) execution of such   |
 | ideal parallel programs on fault-prone parallel machines.                  |
 |                                                                            |
 | There has been a lot of recent activity in this area, addressing a variety |
 | of issues.  The main concerns of these efforts fall into two categories.   |
 | First, research has been directed towards the design of general strategies |
 | for deriving resilient computations, that work independent of any          |
 | particular parallel program.  Second, these strategies are extremely       |
 | efficient in that the overhead they introduce into the resilient           |
 | computation, relative to the ideal program from which it is derived, is    |
 | provably small.  Furthermore, these strategies are fully automatic and can |
 | be applied as compile-time transformations to the ideal program.           |
 |                                                                            |
 | The ideal programming model that we will be considering is that of a       |
 | completely reliable shared-memory parallel machine in which the processors |
 | can execute in perfect lock-step synchrony, if needed.  The canonical      |
 | fault-prone machine on which these programs will actually be executing, is |
 | one in which the set of resources (including processors) that are assigned |
 | to the program, fluctuate dynamically during its execution. These          |
 | fluctuations could be induced by phenomena such as failures and repairs,   |
 | or due to rescheduling by the operating system.  We will be discussing     |
 | transformations that are applicable in the context of shared memory, as    |
 | well as distributed-memory implementations of these fault-prone parallel   |
 | machines.                                                                  |
 |                                                                            |
 `----------------------------------------------------------------------------'