Strategic Directions in Computing Research
Concurrency Working Group Report

Edited by:

Rance Cleaveland Scott A. Smolka
Department of Computer Science Department of Computer Science
North Carolina State University State University of New York at Stony Brook
Raleigh, NC 27695-8206 Stony Brook, NY 11794-4400
rance@csc.ncsu.edu sas AT cs DOT sunysb DOT edu

Working Group Members:

Rajeev Alur (U. California Berkeley) Dale Miller (U. Pennsylvania)
Jos Baeten (Technical U. Eindhoven) Jay Misra (U. Texas Austin)
Jan Bergstra (U. Amsterdam) Faron Moller (Uppsala Univ.)
Eike Best (U. Hildesheim) Ugo Montanari (U. Pisa)
Rance Cleaveland (N.C. State Univ.) Amir Pnueli (Weizmann Univ.)
Rocco De Nicola (U. Firenze) Sanjiva Prasad (IIT Delhi)
Helen Gill (Mitre Corp.) Vaughan Pratt (Stanford Univ.)
Roberto Gorrieri (U. Bologna) Joseph Sifakis (VERIMAG Grenoble)
Mohamed Gouda (U. Texas Austin) Scott A. Smolka - Chair (SUNY Stony Brook)
Jan Friso Groote (CWI) Bernhard Steffen (U. Passau)
Tom Henzinger (U. California Berkeley) Bent Thomsen (ICL)
C.A.R. Hoare (Oxford Univ.) Frits Vaandrager (U. Nijmegen)
Maj. David Luginbuhl (AFOSR) Moshe Vardi (Rice Univ.)
Albert Meyer (MIT) Pierre Wolper (U. Liège)

1 Introduction

Concurrency is concerned with the fundamental aspects of systems of multiple, simultaneously active computing agents that interact with one another. This notion is intended to cover a wide range of system architectures, from tightly coupled, mostly synchronous parallel systems, to loosely coupled, largely asynchronous distributed systems. We refer to systems exhibiting concurrency as concurrent systems, and we call computer programs written for concurrent systems concurrent programs.

Concurrency has emerged as a separate area of research in response to the intrinsic difficulties experienced by designers of concurrent systems in diverse fields within computer science. These difficulties stem in general from two main sources. The first is that the presence of multiple threads of control can lead to subtle and often unanticipated interactions between agents--in particular, issues such as interference, race conditions, deadlock, and livelock are peculiar to concurrent programming. The second arises from the fact that many concurrent systems, such as operating systems and distributed databases, are reactive, meaning that they are designed to engage in an ongoing series of interactions with their environments. Unlike traditional sequential programs, reactive systems should not terminate, and consequently traditional notions of correctness that rely on relating inputs to expected outputs upon termination no longer apply. Developing mathematical frameworks that accurately and tractably account for these phenomena has been a major goal of researchers in concurrency.

This report focuses on research into models and logics for concurrency and their application in specifying, verifying, and implementing concurrent systems. This general area has become known as concurrency theory, and its roots may be traced back to the 1960s [Dij68, Pet62]. Our aim is to survey the rich collection of mature theories and models for concurrency that exist; to review the powerful specification, design, and verification methods and tools that have been developed; and to highlight ongoing active areas of research and suggest fruitful directions for future investigation.

By focusing on concurrency theory and its use in verification, we necessarily omit consideration of other concurrency-related topics such as concurrency control in database systems, concurrent program debugging, operating systems, distributed system architecture, and real-time systems. The interested reader is referred to other working group reports, which address many of these topics.

The remainder of this report develops along the following lines. The next section discusses the current state of concurrency research; the section following then presents strategic directions for future investigation. Finally, some concluding remarks are given.

2 Concurrency Research - The State of the Art

 

This section gives an overview of the current state of research in concurrency. It reviews work on mathematical models of concurrency, discusses results obtained in system specification and verification, and surveys the practical impact of concurrency theory.

2.1 Models for Concurrency

 

As the introduction suggests, concurrent systems differ in essential ways from sequential ones. In order to characterize the fundamental aspects of these systems, researchers have developed a variety of mathematical theories of concurrency over the past two decades. It should first be noted, however, that there is a basic agreement between the different schools of thought: unlike the semantic theories developed for sequential computation, models of concurrent systems cannot be viewed as mappings from inputs to outputs, owing to the reactive nature of such systems as well as their capacity for nondeterminism. Instead, it is necessary to take into account the fact that systems interact with other systems and hence may exhibit patterns of stimuli/response relationships that vary over time. Consequently, rather than adopting the notion of input/output mapping as primitive, theories of concurrency are generally based on the assumption that certain aspects of system behavior are atomic. Systems then execute by engaging in patterns of these ``indivisible'' events.

The point of departure for different theories of concurrency lies in what constitute ``patterns'' of events. More specifically, models that have been developed may be classified on the basis of the stances they adopt with respect to three basic dichotomies.

The first dichotomy also arises in the semantics of sequentiality, but the last two are peculiar to concurrency. We elaborate on each of these below.

Intensionality vs. extensionality.

Intensional models focus on describing what systems do, while extensional models are based on what an outside observer sees. Consequently, intensional theories are sometimes referred to as operational, while extensional ones are called denotational, the denotation of a process being the set of observations it can engender.

Intensional theories model systems in terms of states and transitions between states. In labeled transition systems [Kel76] transitions are decorated with atomic actions representing interactions with the environment; these have been studied extensively in the context of process algebras such as ACP [BW90], CCS [Mil89] and CSP [Hoa85]. I/O automata [LT89] also follow this approach, but they additionally allow distinctions to be made between different kinds of actions (inputs and outputs). Petri nets [Rei85] extend the state/transition paradigm by allowing states to be ``distributed'' among different locations. UNITY [CM88] adopts an imperative style, with transitions corresponding to the (atomic) execution of conditional assignment statements.

In contrast, extensional models first define a notion of observation and then represent systems in terms of the observations that may be made of them. One of the most basic observations about a system is a trace, or sequence of atomic actions executed by a system [Hoa85]. Elaborations of this model include acceptance trees [Hen88] and failure sets [BHR84], both of which decorate basic trace information with information about what stimuli systems may respond to after performing a sequence. Synchronization trees [Mil80] encode system behavior as a tree with edges labeled by actions. Mazurkiewicz traces [Maz87] include an independence relation between actions to capture possible concurrency. Kahn nets [Kah74] define the behavior of dataflow systems, whose components are given by I/O equations, using fixed-point theory. Other models, such as pomsets [Pra86], encode concurrency information using partial orders on atomic events possibly enriched with a conflict relation (event structures [Win89]) to encode information about choices made during execution.

Interleaving vs. true concurrency.

Interleaving models ``reduce'' concurrency to nondeterminism by treating the parallel execution of actions as the choice between their sequentializations. This view may be termed a ``uniprocessor'' approach to concurrency. To avoid anomalies having to do with process starvation, fairness constraints are sometimes imposed to ensure that individual processes ``make progress'' if they are capable of doing so [Fra86]. Theories such as ACP, CCS and CSP employ interleaving, as do I/O-automata and UNITY; both of the latter also include mechanisms for enforcing fairness constraints. The trace-based and synchronization-tree extensional models also cater for modeling concurrency via interleaving.

In contrast, truly concurrent models instead treat concurrency as a primitive notion; the behavior of systems is represented in terms of the causal relations among the events performed at different ``locations'' in a system. Petri nets represent concurrency in this manner, as do Kahn nets, Mazurkiewicz traces, pomsets and event structures.

Branching time vs. linear time.

The difference between branching-time and linear-time models lies in their treatment of the choices that systems face during their execution. Linear-time models describe concurrent systems in terms of the sets of their possible (partial) runs while in branching-time models the points at which different computations diverge from one another is recorded. Thus traces and pomsets are linear-time models while synchronization trees and event structures are branching-time theories.

Discussion.

Different decisions about the three dichotomies are appropriate for different purposes. Extensional models provide a useful basis for explaining system behavior, while intensional ones are often more amenable to automated analysis, as they typically give rise to (finite-)state machines. An interleaving semantics is useful for specifying systems, whereas a truly concurrent semantics might be the basis for describing possible implementations, where for example performance issues are of interest. A branching-time semantics is useful for modeling future behavior of a system, while linear-time suffices for describing execution histories.

While traditional theories have concerned themselves with modeling choice and concurrency, more recent work has focused on elaborating them with other aspects of system behavior, including real-time, probability and security. This point is addressed in more detail in Section 3.1.

2.2 Verification Formalisms

 

In dealing with concurrent programs care must be taken when defining the notion of ``correctness''. Traditional (deterministic) sequential programs may be viewed as (partial) functions from inputs to outputs; in such a setting specifications may be given as a pair consisting of a precondition describing the ``allowed'' inputs and a postcondition describing the desired results for these inputs. This notion of specification remains appropriate for a concurrent program representing a ``parallelized'' version of some sequential program; in this case, concurrency (parallelism) has been introduced solely for performance purposes. For reactive, nonterminating and potentially nondeterministic concurrent systems, however, this approach is too limited. This section presents alternative notions that have been developed and discusses related approaches for reasoning about systems.

2.2.1 Specification

Two general schools of thought have emerged regarding appropriate mechanisms for specifying concurrent systems. One emphasizes the use of logical formulas to encode properties of interest; another uses ``high-level'' systems as specifications for lower-level ones. What follows elaborates on each of these.

Logics for Concurrency.

In a seminal paper [Lam77], Lamport argued that the requirements that designers wish to impose on reactive systems fall into two categories. Safety properties state that ``something bad never happens''; a system meeting such a property must not engage in the proscribed activity. Liveness properties, on the other hand, state that ``something good eventually happens''; to satisfy such a property, a system must engage in some desired activity. Although informal, this classification has proved enormously useful, and formalizing it has been a main motivation for much of the work done on specification and verification of concurrent systems. Some of this work has aimed at semantic characterizations of these properties [AS85]. Others have developed logics that allow the precise formulation of safety and liveness properties. The most widely studied are temporal logics, which were first introduced into the computer science community by Pnueli [Pnu77] and support the formulation of properties of system behavior over time. The remainder of this section reviews some of the research into temporal logic.

The dichotomies presented earlier in modeling concurrency also reveal themselves in the development of temporal logics. In particular, two schools of temporal logic have emerged [EH86].

Linear-time
logics permit properties to be stated about the execution sequences a system exhibits.
Branching-time
logics allow users to write formulas that include some sensitivity to the choices available to a system during its execution.

Numerous variants of linear-time and branching-time temporal logic have been proposed, as researchers have investigated operators that ease the formulation of properties in different settings [MP91]. The expressiveness of these formalisms has also been compared and contrasted [EH86], and a (in some sense) canonically expressive temporal logic, the modal mu-calculus [Koz83], has been developed.

The other two dichotomies--intensional vs. extensional, and interleaving vs. true concurrency--remain relatively unexplored. Traditional temporal logics have generally adopted an extensional view of system behavior and an interleaving model of concurrency, although recent work has explored logics for true concurrency [Thi94].

Finally, other logics have also been developed for reasoning about concurrent systems, including various dynamic logics and logics of knowledge. The former permit the inclusion of programs inside formulas [Pel87], while the latter allow users to express the understanding that individual agents have of other agents' states at a given point in time [HM90, HZ92].

Behavioral Relations.

Another popular approach to specifying concurrent systems involves the use of behavioral equivalences and preorders to relate specifications and implementations. In this framework, which was introduced by Milner [Mil80] and has been extensively explored by researchers in process algebra [BW90, Hoa85, Mil89], specifications and implementations are given in the same notation; the former describes the desired high-level behavior, while the latter provides lower-level details indicating how this behavior is to be achieved. In equivalence-based methodologies, proving an implementation correct amounts to establishing that it behaves ``the same as'' its specification; in those based on preorders, one instead shows that the implementation provides ``at least'' the behavior dictated by the specification.

In support of this approach, a number of different equivalences and preorders have been proposed based on what aspects of system behavior should be observable. Relations may be classified on the basis of the degree to which they abstract away from internal details (viz. the intensional/extensional dichotomy) of system descriptions; the amount of sensitivity they display to choices systems make during their execution (viz. the linear/branching time dichotomy); and the stance they adopt with respect to interleaving vs. true concurrency. For example, bisimulation equivalence [Mil80] is a branching-time, interleaving-based, intensional equivalence, while observational equivalence [Mil80] is a branching-time, interleaving-based extensional equivalence. Other noteworthy relations include the failures/testing relations (linear-time, interleaving, extensional) [BHR84, DNH84] and pomset equivalence (linear-time, truly concurrent, extensional) [Pra86]. Interested readers are referred to [Gla90] for a detailed study of the relationship among different equivalences.

These relations may also be used to bridge the gap between intensional and extensional models of concurrency described above. That is, in order to define a relation over intensional models, one first selects the extensional, or ``observable'', information that processes may exhibit and then uses this as the basis for relating models.

Comparison.

The chief distinction between the two specification approaches arises in the amount of information they require users to specify. Logic-based approaches support very loose specifications, as one is allowed to identify single properties that systems should have. System-based approaches require fairly complete specifications of required observable behavior, although in this respect preorders generally allow looser specifications than equivalences. On the other hand, behavioral relations provide support for step-wise refinement of systems as well as compositional approaches to analyzing system behavior, which temporal logics in general do not, since the specification and system notations differ.

Connections between the two approaches have also been explored. In particular, a temporal logic induces an equivalence on systems as follows: two system are equivalent if and only if they satisfy the same formulas. Using this framework, relationships between different linear- and branching-time logics and equivalences have been established [HM85, BCG88].

2.2.2 Verification Methodologies and Algorithms

 

Verification refers to the process of establishing that a system satisfies a specification given for it. The previous subsections described different approaches to specifying concurrent systems; this one gives an overview of techniques of establishing that systems meet such specifications.

Proof systems.

One verification methodology involves using axioms and inference rules to prove that systems satisfy specifications. Researchers have investigated proof systems for several different specification formalisms, including variants of temporal logic and a variety of behavioral relations, and we briefly review these here.

Early proof systems aimed at generalizing frameworks for sequential programs to cope with concurrency [OG76]. In particular, specifications were given as pairs of conditions circumscribing the allowed inputs and desired outputs, and consequently reactive systems were not catered for. However, it was in the context of this work that interference emerged as a crucial complicating factor in verifying concurrent programs. To cope with nonterminating systems, other researchers focused their attention to developing proof methodologies for establishing that systems satisfied different specifications given as invariants [Lam80].

Traditional temporal-logic-based proof systems rely on proving implications between temporal formulas [Pnu77]. To prove a system correct, one first translates it into an ``equivalent'' temporal formula and proves that this formula entails the specification. The virtue of this approach is that one can use (existing) axiomatizations of temporal logic to conduct proofs; the disadvantage is the translation requirement, which usually obscures the structure of the system. More recent proof systems such as UNITY [CM88] adopt proof rules for specific system notations and temporal logics; other work has been devoted to the development of domain-specific rules for establishing certain classes of properties [MP91, MP95].

Behavioral-relation-based proof systems have typically been algebraic (hence the term process algebra) [Mil89, BW90]; in order to prove that two systems are equivalent, one uses equational reasoning. Sound and complete proof system have been devised for a number of different equivalences, preorders, and description languages.

Algorithms.

Finite-state systems turn out to be amenable to automatic verification, since their observable behavior can be finitely represented. These systems arise in practice in areas such as hardware design and communication protocols; this fact has spurred interest in the development of verification algorithms for temporal logic and relation-based specifications.

The task of determining automatically whether a system satisfies a temporal formula is usually referred to as model checking. One may identify two basic approaches to model checking. The first, which grew out of the branching-time logic community, relies on an analysis of the structure of the formula to determine which system states satisfy the formula [CES86, CS93]. The second, which arose from the linear-time community, is automaton-based [VW86]; one constructs an automaton from the negation of the formula in question and then determines whether or not the ``product'' of this automaton and the automaton representing the system is empty (if so, the system is correct). The two approaches turn out to be related, and indeed automaton-based approaches have been developed for branching-time logics and ``structure-based'' ones have been devised for linear-time logics [BVW94, BCG95]. The time complexities of the best algorithms in each case are proportional to the product of the number of system states and the size of the formula (branching-time) or an exponential of the size of the formula (linear-time).

Algorithms have also been devised for determining whether systems are related by semantic relations. Traditional approaches for calculating equivalences combine partition-based algorithms for bisimulation equivalence [PT87, KS90] with automaton transformations that modify the automata corresponding to the systems being checked [CPS93]. Methods for computing preorders follow a similar scheme, with the ``base'' relation being a variant of the simulation preorder.

The key impediment to the practical application of these algorithms is the state-explosion problem. In general, the number of states a system has will be exponential in the number of concurrent processes; thus, as the number of processes grows, the possibility of enumerating all possible system states rapidly becomes infeasible. Much of the recent work on model and relation checking has been devoted to techniques for ameliorating the effects of state explosion. Some of the techniques that have been developed include:

Symbolic representations
of state spaces via e.g. binary decision diagrams [BCM+92], as a means of encoding system states more compactly;
On-the-fly algorithms
rely on a demand-driven generation of states to avoid the construction of irrelevant system configurations [And94, BCG95];
Redundancy elimination
strives to reduce the number of redundant system states that algorithms analyze, and includes partial-order reduction techniques [Val92, GW93, Pel96, GPS96], semantic minimization [RdS90], and symmetry-based approaches [CFJ93, ES93].

Finally, researchers have also developed techniques for handling certain kinds of infinite-state systems, including context-free processes [BBK93] and those based on dense real-time [AD94].

2.2.3 Tools

The past decade has also witnessed the development of tools that use concurrency theory as a basis for automating the design and analysis of concurrent systems. What follows is essentially a categorization of tools based on the degree of interaction demanded from the user during the verification process. The interested reader is also referred to the report of the formal methods working group for additional tool information.

Interactive Tools.

These typically employ a theory for reasoning about concurrent systems in conjunction with a deduction engine to allow users to conduct proofs that systems enjoy certain properties. The virtue of such tools is that they permit the analysis of systems--such as those that are parameterized or manipulate data--that lie beyond the scope of fully automated tools; their disadvantage is that they can require substantial user interaction. Sample tools include PVS [ORS92] and Coq/muCRL [BG93], which both enrich type theories for manipulating values with notions of concurrency and which have been used to prove the correctness of parameterized systems and distributed algorithms and protocols; STeP [BBC+96], which provides automated support for establishing that concurrent systems satisfy temporal formulas as well as a decision procedure for temporal logic and a model checker; and PAM [Lin91], which oversees the construction of algebraic proofs of equivalence between terms in a process algebra that the user specifies.

Automatic tools.

These provide implementations of one or more of the verification algorithms discussed above. The chief virtue of these tools is that they are automatic; the disadvantage is that the classes of system that may be analyzed are restricted to those having some appropriate finitary representation. Sample tools include SPIN [HP96] and COSPAN [HHK96], which support model checking in linear-time formalisms; the Concurrency Workbench [CPS93], FDR [Ros94] and AUTO [RdS90], which compute various semantic relations and (in the case of the Workbench) implement branching-time model checkers; and Xesar [QS82] and SMV [CMCHG96], which support branching-time model checking. UV [Kal96] is a model-checker for UNITY that combines automatic checking of linear-time temporal properties with interactive features that allow a user to supply hints for speeding up the checking procedure. PEP [GB96] allows the automatic analysis of Petri-net-based systems. Other tools have been developed for verifying real-time and hybrid systems, including HyTech [HHWT95], Kronos [DY95] and UppAal [BLL+96]; and for checking security properties [FG96]. Some tools, such as Statemate [HLN+90] and the Concurrency Factory [CGL+94], also provide support for the generation of code from system models.

Metatools.

The multitude of concurrency models and verification formalisms has also spurred interest in the development of metatools that support the customization and collaborative use of existing tools. Examples include PAM [Lin91], which allows users to change the process algebra and equational axiomatization being used; the Process Algebra Compiler [CMS95], which may be used to generate new front ends for the Concurrency Workbench; and MetaFRAME [SMCB96], which provides a framework for integrating tools so that they may be used in conjunction with one another.

2.2.4 Applications

 

The remainder of Section 2 reviews some of the applications in the area of programming languages and system verification to which concurrency theory has been put.

Concurrent programming languages.

Traditionally, the inclusion of concurrency into programming languages has been done in a somewhat ad hoc manner; the general paradigm has been to augment sequential languages such as C with facilities for using operating-system-supplied primitives such as process creation and semaphores. This meant that programs written in these programs were not portable across different operating systems; in addition, the low-level nature of system calls led to programs that were difficult to maintain.

Programming language researchers have over the past decade begun to investigate the design of programming constructs based on models of concurrency described above as a means of remedying this problem. Examples include OCCAM [Inm88], which arose out of the work done on CSP [Hoa85]; synchronous programming languages such as ESTEREL [BG92] and LUSTRE [Hal93], which evolved from dataflow models [Kah74, KM77]; and PICT [PT95a, PT95b], CML [Rep92], and Facile [TLK96], which are functional concurrent programming languages based on process algebras (CCS [Mil89], pi-calculus [MPW92]), and their higher-order extensions (Higher Order pi-calculus [San92, San93] and CHOCS [Tho89, Tho93, Tho95]). Other languages, such as Linda [CG89], have been given rigorous semantics using techniques borrowed from concurrency theory [DNP94, JW94]. See Section 3.4 for a discussion of the use of concurrency models in programming language design as a strategic research direction.

System verification.

Significant case studies to which concurrency theory has been brought successfully to bear are too numerous to give a complete account of. What follows lists ones taken from a forthcoming special issue of the journal Science of Computer Programming devoted to industrial applications; the interested reader is also referred to the formal methods report for others.

3 Strategic Directions

We present a number of strategic directions for future concurrency research, each of which is accompanied by a ``grand challenge''. The challenges are intended to serve as a yardstick for progress made along the various research directions.

3.1 Beyond Correctness

  In sequential programming, researchers studying semantic issues have focused most of their attention on program correctness, which can be modeled as a function relating inputs to outputs. A correct sequential program should also terminate for all inputs. See [AA78, dB80, Apt81, Apt84, Jon92] for comprehensive coverage of proof techniques for sequential programs. Program efficiency (space and time) has also received tremendous attention (see the ACM SDCR Theory of Computation working group report.)

For concurrent systems, particularly those of the reactive variety, many non-functional requirements are of interest to system builders. These include the following:

Timeliness.
Many concurrent systems are subject to timing constraints, e.g., if the amount of water in a water pump exceeds a certain level then the pump should shut off within t seconds. Embedded systems, which interact with their environment through sensors and actuators, are a typical example of a class of concurrent systems for which real-time behavior is a major concern and performance requirements must be met.
Fault tolerance.
Concurrent systems must often provide reliable service despite the occurrence of various types of failures. Such fault-tolerance is invariably achieved through redundancy of system components [GR92].
Probability.
Although not a requirement per se, equipping specifications with probability information can be useful for specifying system fault characteristics, e.g., the rate at which a faulty communications channel drops messages.
Continuous behavior.
A hybrid system consists of a non-trivial mixture of discrete and continuous components, such as a digital controller that controls the continuous movement of control rods in a nuclear reactor.
Security.
As systems become more distributed and more accessible, it is increasingly important to make them resistant to passive or active misuse by intruders.
Mobility.
Mobile processes are processes that can exchange communication links, thereby introducing the possibility of dynamically reconfigurable network architectures. Mobile processes, which are closely related to higher-order processes, permit process passing.

Note that these different types of requirements are sometimes contradictory. Reliability, for instance, requires the use of additional resources, which may degrade system performance and thus endanger timeliness (see [KS92, KMS94] for a treatment of the reliability vs. efficiency tradeoff in parallel programs).

Recognizing their importance, concurrency researchers have been turning their attention more and more to the non-functional requirements of concurrent programs. For example, substantial progress has been made on models and logics for real-time [Zub80, RR88, NRSV90, BB91, ZHR91, HMP91, MMP92, AD94], probability [Han94, LS92, SL94, GSS95, BG96], mobility [MPW92, Tho93, San92, MPW93, San93, Hen93, Tho95, ACS96] and hybrid systems [ACHH93, MP93, Hoo93, NOSY93, Lam93, ACH+95, HH95, Ver95, LSVW96].

Challenge:

Solidify our understanding of phenomena such as real-time and mobility and at the same time develop new formalisms for those phenomena that remain largely unexplored (e.g., security, although see [FG95, Ros95a]). Achieving these goals will likely necessitate interaction with researchers from other computer science disciplines (security experts, system engineers, etc.), and from non-computer-science disciplines such as electrical and mechanical engineering and control theory.

We should also strive to develop semantic partnerships between formalisms that would facilitate the construction of a model that captures the requirements most relevant to a given problem; e.g., a model that embodies timing and probability information in the context of mobile systems (see also Section 3.2, which treats, in greater detail, the challenge of taxonomizing and unifying semantic models of concurrency).

Finally, these formalisms must be brought out of the ``test-tube'' environment and applied in an integrated way to the specification, verification and design of complex real-life systems. A concrete challenge here is the formal modeling and analysis of the emerging micro electro-mechanical systems (MEMS) technology, which presents a host of modeling challenges. The interested reader should see [Gab95] and the ACM SDCR MEMS working group report for more on MEMS.

Another challenging application is air-traffic control. Its safety-critical nature and high degree of concurrency, make this area an ideal test-case for concurrency research. The utility of a formal approach is already evident in the work [HL96], where a formal requirements specification of the commercial traffic collision avoidance system (TCAS II) was produced and tested. Greater challenges lie in the future, particularly if today's centralized solutions that require airplanes to use specific approach patterns to runways are abandoned in favor of decentralized ``free-flight'' solutions. While free-flight solutions can improve efficiency and solve congestion problems, the complexity of their design demands use of formal approaches. Principal to this design are problems of coordination and conflict resolution among multiple agents [SMT+95].

3.2 A Unifying Semantic Framework of Concurrency

 

The progress of science involves a constant interplay between diversification and unification. Diversification extends the boundaries of science to cover new and wider ranges of phenomena; successful unification reveals that a range of experimentally validated theories are no more than particular cases of some more general principle. The cycle continues when the general principle suggests further specialisations for experimental investigation.

From C.A.R. Hoare's position statement

During the past twenty years, concurrency theory has produced a mature but loose collection of models, theorems, algorithms, and tools. The collection is mature because it is based on a solid mathematical foundation (see Section 2.1) and has made possible documented successes in system design and analysis (see Section 2.2.4). The collection is loose because a theoretical result or a practical application is typically carried out within a particular formalism, whose idiosyncrasies may support the result or application in undeclared ways.

Overall, the myriad of formalisms has led to healthy diversity rather than fragmentation of the discipline: existing concurrency theories have proved suitable for a wide range of application domains, and comparative concurrency theory [Win87, Gla90, Old91, Abr96] has identified deep mathematical relationships between individual theories.

Yet, potential users, such as designers of communication protocols and embedded systems, have been reluctant in applying concurrency-theoretic methods. This reluctance is reinforced by the perceived need of having to buy into one particular formalism and tool from what must seem, to the bystander, a bewildering array of choices.

Challenge:

Develop a systematic and coherent way of presenting concurrency theory to its potential users. This should be achieved by a simple uniform framework that permits an application-oriented taxonomy of the major models of concurrency and a structured organization of the core results.

A uniform framework for concurrency will aid not only potential users of concurrency-theory-based tools, but also students and researchers. In particular, such a framework could provide a basis for concurrency education in the computer science curriculum (see Section 3.5). It could also aid the development of new methods and tools for the design and analysis of heterogeneous systems, consisting of synchronous and asynchronous, discrete and continuous, hardware and software components. For example, a sufficiently broad framework could support the implementation of asynchronous protocols using synchronous circuits.

The literature already contains a myriad of proposals for highly abstract, general-purpose models of concurrency, e.g., [GV92, BDH92, BH93, Mil93, Gla93, ABV94, WN95, MMP95, MR96, Abr96, AH96b], and the uniform framework we seek could very well evolve from this body of work. To make this discussion more concrete, and to illustrate the rich diversity among the proposed models, we briefly describe three of these efforts.

A reactive module [AH96b] is a kind of state transition system that has been proposed as a uniform framework for synchronous and asynchronous computation in the context of hardware-software codesign. It supports an abstraction operator that can be used to collapse an arbitrary number of consecutive computation steps into a single step, thereby providing the ability to turn an asynchronous system into a synchronous one (temporal scalability). It supports a hiding operator that changes external variables into internal ones, which can be used to change a synchronous system into an asynchronous one (spatial scalability). Finally, the model is equipped with a natural notion of composition that permits compositional reasoning, i.e., the ability to reason about a composite system in terms of the system components.

Causal computing [MR96] is a general framework for concurrent computation based on the ``true concurrency'' concurrency model. In the causal approach, concurrent computations are defined as those equivalence classes of sequential computations that are obtained by executing concurrent events in any order. A causal program consists of a set of rewriting rules, events are rule applications, and simultaneous rewritings correspond to concurrent events. Causal computing has been used as a model of computation for process algebras, constraint and logic programming, term and graph rewriting, and mobile and coordination systems. Please see the position statement of Ugo Montanari for a closer look at causal computing.

A Chu space [GP93] is an event-state-symmetric generalization of the notion of event structure consisting of a set of events, a set of states, and a binary relation of occurrence between them. The interpretation of process algebra over event structures extends straightforwardly to Chu spaces, while the language of process algebra expands to include the operations of linear logic, compatibly interpreted. Chu spaces may be equivalently formulated in terms of unfolded Petri nets, propositional theories, or history preserving process graphs [GP95]. Chu spaces are of independent mathematical interest, forming a bicomplete self-dual closed category first studied by Barr and Chu [Bar79] which has found applications elsewhere in proof theory, game theory, and Stone duality [Pra95]. Chu spaces are the subject of Vaughan Pratt's position statement.

3.3 Design and Verification Methodologies

There are two important observations about the current state in the design and verification of concurrent systems:

Challenge:

Transform the existing array of design and verification techniques into sound and tested methodologies. The resulting methodologies should extend the range of existing techniques to applications orders of magnitude larger in size and complexity. Similar to concerns raised in Section 3.2 regarding a uniform semantic framework for concurrency, we should also seek ways to combine methodologies, to better suit the demands of a given application, and, relatedly, develop an application-oriented taxonomy of methodologies.

To produce a next generation of truly usable methodologies, the following issues must be addressed:

Algorithmic support.
Further advances (i.e., beyond those listed in Section 2.2.2) are needed to better cope with the state-space explosion problem inherent to concurrent system design and verification. Compositional methods, in which the analysis of a system is decomposed into an analysis of its components, and refinement methods, in which a system is analyzed at varying levels of abstraction, may play a key role. The issue of algorithmic support is addressed more fully in the position statement of Pierre Wolper.
Tool support.
The problems confronting today's tools, such as lack of portability and scalability, need to be addressed. Furthermore, tools should be better integrated into the software engineering lifecycle. Traditionally, software engineering devotes much attention to organizational and procedural issues in software development and relatively little to methods for system analysis; in this respect, it resembles a management discipline rather than an engineering one. Tools based on concurrency theory offer a particularly appropriate starting point for putting the engineering into software engineering.
Technology Transfer.
The capacity of today's design and verification technology will improve only if subjected to protracted exposure to real-life industrial and government (i.e., defense) applications. The transfer of this technology to these arenas is thus a key issue, and will be facilitated by increased tool support (including improved user interfaces) and education. The role of tool support in technology transfer is the subject of the new Springer-Verlag Journal Software Tools for Technolgy Transfer, to begin publication in September 1997. Education should include training in both tool usage and in the concurrency-theoretic concepts underlying the tools (see Section 3.5). Furthermore, one can expect a domino effect: as companies and agencies achieve positive results in the use of the latest design and verification methodologies, more users are likely to follow suit.

3.4 Programming Languages for Concurrency

 

In Section 2.2.4, we briefly discussed the impact models of concurrency have had on the design of concurrent programming languages. Strategically, we believe that the continued use of concurrency theory--especially as this theory continues to evolve--in the design and implementation of programming languages is an important research direction. The main rationale behind this belief is simple and powerful: the development of programming languages with strong foundations in concurrency theory would blur, and in some cases completely eliminate, the distinction between a system model and a system implementation. As such, the task of designing, coding, and verifying concurrent systems would be significantly eased.

Designing programming languages for concurrency is a nontrivial task. Adding a notion of concurrency to an existing language may break some of the tacit assumptions of the language's design, such as determinism and no (inter-process) interference on variables. Thus, designing a language with an explicit concurrency model from scratch is likely to produce a language with a cleaner and better-understood semantics. Moreover, rooting a programming language in a sufficiently expressive concurrency model could lead to the construction of re-usable abstractions for sophisticated synchronization mechanisms, in much the same way as objects are used in sequential systems today.

A concurrency model underlying the design of a parallel programming language might also increase our ability to efficiently port a program across a wide spectrum of system architectures, without unduly restricting the parallelism in the ported version of the program. Concurrency models by their very nature tend to be abstract, meaning that they are largely architecture-independent. In particular, they typically assume no a priori limit on the number of processors available for running processes (but see [GL94] for an exception), and hence capture a notion of maximal parallelism.

To better address the portability issue, we should more closely examine the interplay between true concurrency models and interleaving-based models (Section 2.1). The former come into play when mapping individual processes to individual processors in the target architecture; the latter are relevant when multiple processes must be mapped to the same processor. A better understanding of this interplay is one of the potential benefits of a unifying framework for concurrency (Section 3.2).

Concurrency theory has also begun to influence the design of type systems for functional concurrent programming. In [NN93, NN94] function types of the form f:t1--b-->t2 are allowed, where b is a process algebra behavior expression. The type is to be read: function f takes a value of type t1 and produces a value of type t2 and in doing so has behavior b. Under some conditions these behaviors will be inferable and ``principal'' in a sense similar to that of SML [MTH90]. A similar approach has been proposed in [Nie90] for concurrent object-oriented languages based on process algebra.

Type systems of this nature seem like a particularly promising technique for integrating a concurrency model into a programming language. For instance, we could devise new type systems that guarantee safety and liveness properties in the same way that traditional type systems guarantee safety in calling functions and procedures [AGN96].

Challenge:

Design usable, safe, and secure languages incorporating a well-understood concurrency model. The need for such languages is particularly urgent now that mobile agents or applets have started to roam the Internet. Currently, mobile agents are written in languages such as Java, Telescript and Safe Tcl/Tk, all providing rudimentary support for concurrency in the form of threads and semaphores. There is, however, a growing need for extending the concurrency constructs of these languages or designing new languages with more advanced synchronization mechanisms, including synchronous channels, multi-cast groups and constraint variables. Concurrency theory--in particular, higher-order and mobile theories [Tho93, Tho95, MPW92, San92, San93, Hen93, NN94]--can play an important role in achieving these goals. The resulting languages would help system designers analyze sophisticated software systems built using mobile agents.

3.5 Concurrency Education

 

It is unlikely that concurrency-based design and verification methodologies will gain wide-spread acceptance until the user community is educated in these methodologies and the concepts underlying them. Concurrency education should start in the undergraduate curriculum. Moreover, as aptly pointed out in [Ros95b], concurrency, whether we recognize it or not, pervades many areas of computer science--e.g., hardware, operating systems, languages, compilers, and algorithms--and an undergraduate well-versed in concurrency basics will be better-prepared for these courses.

Challenge:

Introduce a course on concurrency basics into the official ACM Undergraduate Computer Science Curriculum by the year 2000.

An undergraduate course on concurrency basics (a course entitled ``Concurrency Theory'' may sound too intimidating) should include coverage of the following essential concepts:

4 Conclusions

In this report, we have outlined the current state of the art in concurrency research and proposed strategic directions and challenges for further investigation. We hope that we have convinced the reader that the field of concurrency is thriving. Mature theories and models exist; specification, design, and verification methods and tools are under active development; many successful applications of substantial complexity have been carried out and the potential for further and more sophisticated application is enormous.

The future of computing is interactive and networked, rather than the traditional sequential one. Consequently the role of concurrency theory, which aims at understanding the nature of interaction, will continue to grow.

An active mailing list for the field can be subscribed to by sending e-mail to concurrency@cwi.nl.

Acknowledgements:

This report has benefited from helpful comments from Chris Hankin, Michael Loui, Jack Stankovic, and Peter Wegner. The editorial activities of Rance Cleaveland have been supported in part by ONR Grant N00014-92-J-1582, NSF Grants CCR-9257963 and CCR-9402807, and AFOSR Grant F49620-95-1-0508; and those of Scott Smolka by NSF Grant CCR-9505562 and AFOSR Grants F49620-93-1-0250 and F49620-95-1-0508.

References

AA78
S. Alagic and M. Arbib. The Design of Well-Structured and Correct Programs. Springer-Verlag, 1978.

Abr96
S. Abramsky. Retracing some paths in process algebra. In Proceedings of CONCUR '96 - Seventh Intl. Conf. on Concurrency Theory, volume 1119 of Lecture Notes in Computer Science, pages 1-17. Springer-Verlag, 1996.

ABV94
L. Aceto, B. Bloom, and F. W. Vaandrager. Turning SOS rules into equations. Information and Computation, 111(1):1-52, May 1994.

ACH+95
R. Alur, C. Courcoubetis, N. Halbwachs, T. A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. The algorithmic analysis of hybrid systems. Theoretical Computer Science, 138:3-34, 1995.

ACHH93
R. Alur, C. Courcoubetis, T.A. Henzinger, and P.-H. Ho. Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In Grossman et al. [GNRR93], pages 209-229.

ACS96
R. Amadio, I. Castellani, and D. Sangiorgi. On bisimulations for the asynchronous pi-calculus. In Proceedings of CONCUR '96 - Seventh Intl. Conf. on Concurrency Theory, volume 1119 of Lecture Notes in Computer Science, pages 147-162. Springer-Verlag, 1996.

AD94
R. Alur and D. Dill. The theory of timed automata. TCS, 126(2), 1994.

AGN96
S. Abramsky, S. Gay, and R. Nagarajan. Specification structures and propositions-as-types for concurrency. Springer-Verlag, 1996.

AH96a
R. Alur and T. A. Henzinger, editors. Computer Aided Verification (CAV '96), volume 1102 of Lecture Notes in Computer Science, New Brunswick, New Jersey, July 1996. Springer-Verlag.

AH96b
R. Alur and T. A. Henzinger. Reactive modules. In Proceedings of the 11th IEEE Symposium on Logic in Computer Science, pages 207-218. IEEE Computer Society, 1996.

And94
H. R. Andersen. Model checking and boolean graphs. TCS, 126(1), 1994.

Apt81
K. R. Apt. Ten years of Hoare's logic, a survey, part I. ACM Transactions on Programming Languages and Systems, 3:431-483, 1981.

Apt84
K. R. Apt. Ten years of Hoare's logic, a survey, part II: Nondeterminism. Theoretical Computer Science, 28:83-109, 1984.

AS85
B. Alpern and F. B. Schneider. Defining liveness. Information Processing Letters, 21:181-185, 1985.

Bar79
M. Barr. *-Autonomous categories, volume 752 of Lecture Notes in Mathematics. Springer-Verlag, 1979.

BB91
J. C. M. Baeten and J. A. Bergstra. Real-time process algebra. Formal Aspects of Computing, 3(2):142-188, 1991.

BBC+96
N. Bjorner, A. Browne, E. Chang, M. Colon, A. Kapur, Z. Manna, H. B. Sipma, and T. E. Uribe. STeP: Deductive-algorithmic verification of reactive and real-time systems. In Alur and Henzinger [AH96a], pages 415-418.

BBK93
J. C. M. Baeten, J. A. Bergstra, and J. W. Klop. Decidability of bisimulation equivalence for processes generating context-free languages. Journal of the ACM, 40:653-682, 1993.

BCG88
M. C. Browne, E. M. Clarke, and O. Grümberg. Characterizing finite Kripke structures in propositional temporal logic. Theoretical Computer Science, 59(1,2):115-131, 1988.

BCG95
G. Bhat, R. Cleaveland, and O. Grumberg. Efficient on-the-fly model checking for CTL*. In Tenth Annual Symposium on Logic in Computer Science (LICS '95), pages 388-397, San Diego, July 1995. Computer Science Press.

BCM+92
J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 10**20 states and beyond. Information and Computation, 98(2):142-170, June 1992.

BDH92
E. Best, R. Devillers, and J. G. Hall. The Petri box calculus: a new causal algebra with multilabel communication. In G. Rozenberg, editor, Advances in Petri Nets 1992, volume 609 of Lecture Notes in Computer Science, pages 21-69. Springer-Verlag, 1992.

BG92
G. Berry and G. Gonthier. The ESTEREL synchronous programming language: design, semantics, implementation. Science of Computer Programming, 19(2):87-152, November 1992.

BG93
M. Bezem and J. F. Groote. A formal verification of the alternating bit protocol in the calculus of constructions. Logic Group Preprint Series 88, Dept. of Philosophy, Utrecht University, March 1993.

BG96
M. Bernardo and R. Gorrieri. Extended Markovian Process Algebra. In U. Montanari, editor, Proceedings of CONCUR'96 volume 1119 of Lecture Notes in Computer Science, pages 315-330. Springer-Verlag, 1996.

BH93
E. Best and R. P. Hopkins. BPNPN - a basic Petri net programming notation. In A. Bode, M. Reeve, and G. Wolf, editors, Proceedings of PARLE'93, volume 694 of Lecture Notes in Computer Science, pages 379-390. Springer-Verlag, 1993.

BHR84
S. D. Brookes, C. A. R. Hoare, and A. W. Roscoe. A theory of communicating sequential processes. Journal of the ACM, 31(3):560-599, July 1984.

BLL+96
J. Bentsson, K. G. Larsen, F. Larsson, P. Pettersson, and W. Yi. UppAal in 1995. In Margaria and Steffen [MS96], pages 431-434.

BVW94
O. Bernholtz, M. Y. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking. In D.L. Dill, editor, Computer Aided Verification (CAV '94), volume 818 of Lecture Notes in Computer Science, pages 142-155, Stanford, California, June 1994. Springer-Verlag.

BW90
J. C. M. Baeten and W. P. Weijland. Process Algebra. Cambridge Tracts in Theoretical Computer Science 18. Cambridge University Press, 1990.

CES86
E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244-263, 1986.

CFJ93
E. M. Clarke, T. Filkorn, and S. Jha. Exploiting symmetry in model checking. In Courcoubetis [Cou93], pages 450-462.

CG89
N. Carriero and D. Gelernter. Linda in context. Communications of the ACM, 32(4):444-458, April 1989.

CGH+95
E. M. Clarke, O. Grumberg, H. Hiraishi, S. Jha, D. E. Long, K. L. McMillan, and L. A. Ness. Verification of the Future+ cache coherence protocol. Formal Methods in System Design, 6:217-232, 1995.

CGL+94
R. Cleaveland, J. N. Gada, P. M. Lewis, S. A. Smolka, O. Sokolsky, and S. Zhang. The concurrency factory -- practical tools for specification, simulation, verification, and implementation of concurrent systems. In G.E. Blelloch, K.M. Chandy, and S. Jagannathan, editors, Proceedings of DIMACS Workshop on Specification of Parallel Algorithms, volume 18 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 75-90, Princeton, NJ, May 1994. American Mathematical Society.

CM88
K. M. Chandy and J. Misra. Parallel Program Design. A Foundation. Addison-Wesley, 1988.

CMCHG96
E. Clarke, K. McMillan, S. Campos, and V. Hartonas-GarmHausen. Symbolic model checking. In Alur and Henzinger [AH96a], pages 419-422.

CMS95
R. Cleaveland, E. Madelaine, and S. Sims. A front-end generator for verification tools. In E. Brinksma, R. Cleaveland, K.G. Larsen, and B. Steffen, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS '95), volume 1019 of Lecture Notes in Computer Science, pages 153-173, Aarhus, Denmark, May 1995. Springer-Verlag.

Cou93
C. Courcoubetis, editor. Computer Aided Verification (CAV '93), volume 697 of Lecture Notes in Computer Science, Elounda, Greece, June/July 1993. Springer-Verlag.

CPS93
R. Cleaveland, J. Parrow, and B. Steffen. The concurrency workbench: A semantics based tool for the verification of concurrent systems. ACM Transactions on Programming Languages and Systems, 1(15):36-72, 1993.

CS93
R. Cleaveland and B. U. Steffen. A linear-time model checking algorithm for the alternation-free modal mu-calculus. Formal Methods in System Design, 2:121-147, 1993.

dB80
J. de Bakker. Mathematical Theory of Program Correctness. Prentice Hall International, Englewood Cliffs, NJ, 1980.

Dij68
E.W. Dijkstra. Cooperating sequential processes. In Programming Languages, pages 43-112, London, 1968. Academic Press. Originally appeared as Technical Report EWD-123, Technical University of Eindhoven, the Netherlands, 1965.

DNH84
R. De Nicola and M. Hennessy. Testing equivalences for processes. Theoretical Computer Science, 34:83-133, 1984.

DNP94
R. De Nicola and R. Pugliese. Testing linda: Observational semantics for an asynchronous language. Rapporto di Ricerca SI/RR-94/06, Dipartimento di Scienze dell'Informazione, Università di Roma ``La Sapienza'', November 1994.

DY95
C. Daws and S. Yovine. Two examples of verification of multirate automata using KRONOS. In 16th Annual IEEE Real-Time Systems Symposium, pages 66-75, Pisa, Italy, December 1995. Computer Society Press.

EH86
E. A. Emerson and J. Y. Halpern. `Sometime' and `not never' revisited: On branching versus linear time temporal logic. Journal of the ACM, 33(1):151-178, 1986.

ES93
E. A. Emerson and A. P. Sistla. Symmetry and model checking. In Courcoubetis [Cou93], pages 463-478.

FG95
R. Focardi and R. Gorrieri. A classification of security properties for process algebras. Journal of Computer Security, 3(1):5-33, 1995.

FG96
R. Focardi and R. Gorrieri. Automatic Compositional Verification of Some Security Properties. In B. Steffen, editor, Proceedings of TACAS'96, volume 1055 of Lecture Notes in Computer Science, pages 167-186. Springer-Verlag, 1996.

Fra86
N. Francez. Fairness. Springer-Verlag, New York, 1986.

Gab95
K. J. Gabriel. Engineering microscopic machines. Scientific American, September 1995.

GB96
B. Grahlman and E. Best. PEP--more than a Petri net tool. In Margaria and Steffen [MS96], pages 397-401.

GL94
R. Gerber and I. Lee. A resource-based prioritized bisimulation for real-time systems. Information and Computation, 113(1):102-142, August 1994.

Gla90
R. J. van Glabbeek. Comparative Concurrency Semantics and Refinement of Actions. PhD thesis, Free University of Amsterdam, 1990.

Gla93
R. J. van Glabbeek. Full abstraction in structural operational semantics. In M. Nivat, C. Rattray, T. Rus, and G. Scollo, editors, Proceedings of the Third AMAST Conference, Twente, The Netherlands, June l993, Workshops in Computing, pages 77-84. Springer-Verlag, 1993.

GNRR93
R. L. Grossman, A. Nerode, A. P. Ravn, and H. Rischel, editors. Hybrid Systems, volume 736 of Lecture Notes in Computer Science. Springer-Verlag, 1993.

GP93
V. Gupta and V. R. Pratt. Gates accept concurrent behavior. In Proc. 34th Ann. IEEE Symp. on Foundations of Comp. Sci., pages 62-71, November 1993.

GP95
R. J. van Glabbeek and G. Plotkin. Configuration structures. In Logic in Computer Science, pages 199-209. IEEE Computer Society, June 1995.

GPS96
P. Godefroid, D. Peled, and M. Staskauskas. Using partial-order methods in the formal validation of industrial concurrent programs. In Proceedings of the 1996 International Symposium on Software Testing and Analysis (ISSTA), San Diego, CA, 1996.

GR92
J. Gray and A. Reuter. Transaction Processing: Concepts and Techniques. Morgan-Kauffman, 1992.

GSS95
R. J. van Glabbeek, S. A. Smolka, and B. Steffen. Reactive, generative, and stratified models of probabilistic processes. Information and Computation, 121(1):59-80, August 1995.

GV92
J. F. Groote and F. W. Vaandrager. Structured operational semantics and bisimulation as a congruence. Information and Computation, 100(2):202-260, October 1992.

GW93
P. Godefroid and P. Wolper. Using partial orders for the efficient verification of deadlock freedom and safety properties. Formal Methods in System Design, 2:149-164, 1993.

Hal93
N. Halbwachs. Synchronous Programming of Reactive Systems. Kluwer Academic Publishers, 1993.

Han94
H. A. Hansson. Time and Probability in Formal Design of Distributed Systems, volume 1 of Real -Time Safety Critical Systems. Elsevier, Uppsala University, Department of Computer Systems, Uppsala, Sweden, 1994.

Har87
D. Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8:231-274, 1987.

Hen88
M. Hennessy. Algebraic Theory of Processes. MIT Press, Cambridge, Massachusetts, 1988.

Hen93
M. Hennessy. A fully abstract denotational model for higher-order processes (extended abstract). In Proceedings Eighth Annual Symposium on Logic in Computer Science, Montreal, Canada, pages 397-408. IEEE Computer Society Press, 1993. Full version in Sussex TR 6/92.

HH95
T.A. Henzinger and P.-H. Ho. Algorithmic analysis of nonlinear hybrid systems. In Proceedings of the 7th International Conference on Computer Aided Verification, Liège, Belgium, Lecture Notes in Computer Science. Springer-Verlag, July 1995.

HHK96
R. Harding, Z. Har'El, and R. Kurshan. COSPAN. In Alur and Henzinger [AH96a], pages 423-427.

HHWT95
T.A. Henzinger, P.-H. Ho, and H. Wong-Toi. HYTECH: The next generation. In 16th Annual IEEE Real-Time Systems Symposium, pages 56-65, Pisa, Italy, December 1995. Computer Society Press.

HL96
M. Heimdahl and N. Leveson. Completeness and consistency in hierarchical state-based requirements. IEEE Trans. Software Engineering, SE-22(6):363-377, 1996.

HLN+90
D. Harel, H. Lachover, A. Naamad, A. Pnueli, M. Politi, R. Sherman, A. Shtull-Trauring, and M. Traktenbrot. Statemate: A working environment for the development of complex reactive systems. IEEE Transactions on Software Engineering, 16(4):403-414, April 1990.

HM85
M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32(1):137-161, 1985.

HM90
J. Halpern and Y. Moses. Knowledge and common knowledge in a distributed environment. Journal of the ACM, 37(3):549-587, July 1990.

HMP91
T. A. Henzinger, Z. Manna, and A. Pnueli. Temporal proof methodologies for real-time systems. In Proceedings of the 18th Annual ACM Symposium on Principles of Programming Languages, pages 353-366, Orlando, FL, January 1991.

Hoa85
C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, London, 1985.

Hoo93
J. Hooman. A compositional approach to the design of hybrid systems. In Grossman et al. [GNRR93], pages 121-148.

HP96
G. Holzmann and D. Peled. The state of SPIN. In Alur and Henzinger [AH96a], pages 385-399.

HZ92
J. Halpern and L. Zuck. A little knowledge goes a long way: Knowledge-based derivations and correctness proofs for a family of protocols. Journal of the ACM, 39(3):449-478, July 1992.

Inm88
INMOS, Ltd. OCCAM-2 Reference Manual, Prentice-Hall International, Englewood Cliffs, NJ, 1988.

Jon92
C. B. Jones. The search for tractable ways of reasoning about programs. Technical Report TR UMCS-92-4-4, Department of Computer Science, University of Manchester, 1992.

JW94
S. Jagannathan and S. Weeks. Analyzing stores and references in a parallel symbolic language. In Proceedings of the ACM Conference on Lisp and Functional Programming, pages 294-305, 1994.

Kal96
M. Kaltenbach. Interactive Verification Exploiting Program Design Knowledge: A Model-Checker for UNITY. PhD thesis, University of Texas at Austin, 1996.

Kah74
G. Kahn. The semantics of a simple language for parallel programming. In J.L. Rosenfeld, editor, Information Processing 74, pages 471-475. North-Holland, 1974.

KM77
G. Kahn and D. B. MacQueen. Coroutines and networks of parallel processes. In B. Gilchrist, editor, Information Processing 77, pages 993-998. North-Holland, 1977.

Kel76
R. Keller. Formal verification of parallel programs. Communications of the ACM, 19(7):371-384, July 1976.

KMS94
P. C. Kanellakis, D. Michailidis, and A. A. Shvartsman. Concurrency = fault-tolerance in parallel computation. In B. Jonsson and J. Parrow, editors, Proceedings of CONCUR '94 -- Fifth International Conference on Concurrency Theory, pages 242-266. Volume 836 of Lecture Notes in Computer Science, Springer-Verlag, 1994.

Koz83
D. Kozen. Results on the propositional mu-calculus. Theoretical Computer Science, 27:333-354, 1983.

KS92
P. C. Kanellakis and A. A. Shvartsman. Efficient parallel algorithms can be made robust. Distributed Computing, 5(4):201-217, 1992.

KS90
P. C. Kanellakis and S. A. Smolka. CCS expressions, finite state processes, and three problems of equivalence. Information and Computation, 86(1):43-68, May 90.

Lam77
L. Lamport. Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering, SE-3(2):125-143, 1977.

Lam80
L. Lamport. The `Hoare logic' of concurrent programs. Acta Informatica, 14:21-37, 1980.

Lam93
L. Lamport. Hybrid systems in TLA+. In Grossman et al. [GNRR93], pages 77-102.

Lin91
H. Lin. PAM: A process algebra manipulator. In K.G. Larsen and A. Skou, editors, Computer Aided Verification (CAV '91), volume 575 of Lecture Notes in Computer Science, pages 136-146, Aalborg, Denmark, July 1991. Springer-Verlag.

LS92
K. G. Larsen and A. Skou. Bisimulation through probabilistic testing. Information and Computation, 94(1):1-28, September 1992.

LSVW96
N. A. Lynch, R. Segala, F. W. Vaandrager, and H. B. Weinberg. Hybrid I/O automata. In R. Alur, T.A. Henzinger, and E.D. Sontag, editors, Hybrid Systems III, volume 1066 of Lecture Notes in Computer Science, pages 496-510. Springer-Verlag, 1996.

LT89
N. A. Lynch and M. R. Tuttle. An introduction to input/output automata. CWI Quarterly, 2(3):219-246, September 1989.

Maz87
A. Mazurkiewicz. Trace theory. In W. Brauer, W. Reisig, and G. Rozenberg, editors, Petri Nets: Applications and Relationships to Other Models of Concurrency, Advances in Petri Nets 1986, Part II; Proceedings of an Advanced Course, Bad Honnef, September 1986, volume 255 of Lecture Notes in Computer Science, pages 279-324. Springer-Verlag, 1987.

Mil80
R. Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer-Verlag, 1980.

MTH90
R. Milner, M. Tofte, and R. Harper. The Definition of Standard ML. MIT Press, Cambridge, Massachusetts, 1990.

Mil89
R. Milner. Communication and Concurrency. International Series in Computer Science. Prentice Hall, 1989.

Mil93
R. Milner. Action calculi, or syntactic action structures. In Proceedings of 19th MFCS, volume 711 of Lecture Notes in Computer Science, pages 105-121. Springer-Verlag, 1993.

MMP92
O. Maler, Z. Manna, and A. Pnueli. From timed to hybrid systems. In J. W. de Bakker, C. Huizing, W. P. de Roever, and G. Rozenberg, editors, Proceedings of the REX Workshop ``Real-Time: Theory in Practice,'' volume 600 of Lecture Notes in Computer Science, Berlin, 1992. Springer-Verlag.

MMP95
A. Mifsud, R. Milner, and J. Power. Control structures. In Proceedings of Tenth Annual IEEE Symposium on Logic in Computer Science, pages 188-198. IEEE Computer Society Press, 1995.

MP91
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1991.

MP93
Z. Manna and A. Pnueli. Verifying hybrid systems. In Grossman et al. [GNRR93], pages 4-35.

MP95
Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, 1995.

MPW92
R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, Parts I and II. Information and Computation, 100, 1992.

MPW93
R. Milner, J. Parrow, and D. Walker. Modal logics for mobile processes. Theoretical Computer Science, 114, 1993.

MR96
U. Montanari and F. Rossi. Graph rewriting and constraint solving for modelling distributed systems with synchronization. In Proceedings of COORDINATION '96. Springer-Verlag, 1996.

MS96
T. Margaria and B. Steffen, editors. Tools and Algorithms for the Construction and Analysis of Systems (TACAS '96), volume 1055 of Lecture Notes in Computer Science, Passau, Germany, March 1996. Springer-Verlag.

Nie90
O. Nierstrasz. Viewing objects as patterns of communicating agents. In Proceedings of ECOOP/OOPSLA'90; European Conference on Object-Oriented Programming/Object-Oriented Programming Systems, Languages and Applications, pages 38-43, 1990.

NN93
F. Nielson and H. R. Nielson. From CML to process algebras. In Proceedings of CONCUR '93 -- Fourth International Conference on Concurrency Theory. Volume 715 of Lecture Notes in Computer Science, Springer-Verlag, 1993.

NN94
H. R. Nielson and F. Nielson. Higher-order concurrent programs with finite communication topology. In Proceedings of 21st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 84-97. ACM Press, 1994.

NOSY93
X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. An approach to the description and analysis of hybrid systems. In Grossman et al. [GNRR93], pages 149-178.

NRSV90
X. Nicollin, J.-L. Richier, J. Sifakis, and J. Voiron. ATP: an algebra for timed processes. In M. Broy and C. B. Jones, editors, Programming Concepts and Methods, pages 415-442, Amsterdam, 1990. North-Holland.

OG76
S. Owicki and D. Gries. An axiomatic proof technique for parallel programs. Acta Informatica, 6:319-340, 1976.

Old91
E.-R. Olderog. Nets, Terms and Formulas: Three Views of Concurrent Processes and Their Relationship. Cambridge Tracts in Theoretical Computer Science 23. Cambridge University Press, 1991.

ORS92
S. Owre, J. Rushby, and N. Shankar. PVS: A prototype verification system. In D. Kapur, editor, 11th International Conference on Automated Deduction (CADE), volume 607 of Lecture Notes in Artificial Intelligence, pages 748-752. Springer-Verlag, June 1992.

Pel87
D. Peleg. Concurrent dynamic logic. Journal of the ACM, 34(2):450-479, April 1987.

Pel96
D. Peled. Combining partial order reductions with on-the-fly model-checking. Formal Methods in System Design, 8(1):39-64, January 1996.

Pet62
C. A. Petri. Kommunikation mit Automaten. Schriften des IIm 2, Institut fur Instrumentelle Mathematik, Bonn, 1962. English translation available as Communication with Automata, Tech. Report RADC-TR-65-377, Vol. 1, Suppl. 1, Applied Data Research, Princeton, NJ 1966.

Plo81
G. D. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, 1981.

Pnu77
A. Pnueli. The temporal logic of programs. In 18th IEEE Symposium on Foundations of Computer Science, pages 46-57. Computer Society Press, 1977.

Pra86
V. R. Pratt. Modeling concurrency with partial orders. International Journal of Parallel Programming, 15(1):33-71, 1986.

Pra95
V. R. Pratt. The Stone gamut: A coordinatization of mathematics. In Logic in Computer Science, pages 444-454. IEEE Computer Society, June 1995.

PT87
R. Paige and R. E. Tarjan. Three partition refinement algorithms. SIAM Journal of Computing, 16(6):973-989, December 1987.

PT95a
B. Pierce and D. Turner. PICT Language Definition. University of Indiana, December 1995. Available at URL http://www.cs.indiana.edu/hyplan/pierce/ftp/pict/.

PT95b
B. C. Pierce and D. N. Turner. Concurrent objects in a process calculus. In Theory and Practice of Parallel Programming, volume 907 of Lecture Notes in Computer Science, Sendai, Japan, April 1995. Springer-Verlag.

QS82
J. P. Queille and J. Sifakis. Specification and verification of concurrent systems in Cesar. In Proceedings of the International Symposium in Programming, volume 137 of Lecture Notes in Computer Science, Berlin, 1982. Springer-Verlag.

RdS90
V. Roy and R. de Simone. Auto/Autograph. In E.M. Clarke and R.P. Kurshan, editors, Computer-Aided Verification '90, volume 3 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 235-250, Piscataway, NJ, June 1990. American Mathematical Society.

Rei85
W. Reisig. Petri Nets - An Introduction. EATCS Monographs on Theoretical Computer Science, Volume 4. Springer-Verlag, 1985.

Rep92
J. H. Reppy. High-order Concurrency. PhD thesis, Cornell University, 1992. Also Cornell Univ. Computer Science Dept. Tech. Report 92-1285.

Ros94
A. W. Roscoe. Model checking CSP. In A Classical Mind: Essays in Honor of C.A.R. Hoare. Prentice-Hall International, 1994.

Ros95a
A. W. Roscoe. CSP and determinism in security modelling. In Proceedings of 1995 IEEE Symposium on Security and Privacy, pages 114-127. IEEE Computer Society Press, 1995.

Ros95b
A. L. Rosenberg. Thoughts on parallelism and concurrency in computing curricula. ACM Computing Surveys, 27(2):280-283, June 1995.

RR88
G. M. Reed and A. W. Roscoe. A timed model for communicating sequential processes. Theoretical Computer Science, 58, 1988.

San92
D. Sangiorgi. Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms. PhD thesis, University of Edinburgh, Edinburgh, Scotland, 1992.

San93
D. Sangiorgi. From pi-calculus to higher-order pi-calculus - and back. In Proceedings of TAPSOFT '93, 1993.

SL94
R. Segala and N. A. Lynch. Probabilistic simulations for probabilistic processes. In B. Jonsson and J. Parrow, editors, Proceedings of CONCUR '94 -- Fifth International Conference on Concurrency Theory, pages 481-496. Volume 836 of Lecture Notes in Computer Science, Springer-Verlag, 1994.

SMCB96
B. Steffen, T. Margaria, A. Classen, and V. Braun. The MetaFRAME '95 environment. In Alur and Henzinger [AH96a], pages 450-453.

SMT+95
S. Sastry, G. Meyer, C. Tomlin, J. Lygeros, D. Godbole, and G. Pappas. Hybrid control in air traffic management systems. In Proceedings of the 34th IEEE Conference on Decision and Control, pages 1478-1483, 1995.

Thi94
P. S. Thiagarajan. A trace based extension of linear time temporal logic. In Ninth Annual Symposium on Logic in Computer Science (LICS '94), pages 438-447, Versailles, France, July 1994. Computer Society Press.

Tho89
B. Thomsen. A Calculus of Higher Order Communicating Systems. In Proceedings of POPL'89. ACM Press, 1989.

Tho93
B. Thomsen. A Second Generation Calculus for Higher Order Processes. Acta Informatica 30, pages 1-59, 1993. Preliminary version in Technical Report 89/04, Imperial College 1989.

Tho95
B. Thomsen. A theory of higher order communicating systems. Information and Computation, 116(1):38-57, January 1995.

TLK96
B. Thomsen, L. Leth, and T.-M. Kuo. A Facile tutorial. In Proceedings of CONCUR '96 - Seventh Intl. Conf. on Concurrency Theory, volume 1119 of Lecture Notes in Computer Science, pages 278-298. Springer-Verlag, 1996.

Val92
A. Valmari. A stubborn attack on state explosion. Formal Methods in System Design, 1(4):297-322, December 1992.

Ver95
J.J. Vereijken. A process algebra for hybrid systems. In A. Bouajjani and O. Maler, editors, Proceedings Second European Workshop on Real-Time and Hybrid Systems, Grenoble, France, June 1995.

VW86
M. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Symposium on Logic in Computer Science (LICS '86), pages 332-344, Cambridge, Massachusetts, June 1986. Computer Society Press.

Win87
G. Winskel. Petri nets, algebras, morphisms, and compositionality. Information and Computation, 72:197-238, 1987.

Win89
G. Winskel. An introduction to event structures. In J.W. de Bakker, W.P. de Roever, and G. Rozenberg, editors, REX School and Workshop on Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, Noordwijkerhout, The Netherlands, May/June 1988, volume 354 of Lecture Notes in Computer Science, pages 364-397. Springer-Verlag, 1989.

WN95
G. Winskel and M. Nielsen. Models for concurrency. In S. Abramsky, D. Gabbay, and T.S.E. Maibaum, editors, Handbook of Logic in Computer Science, Vol. 4, pages 1-148. Oxford University Press, 1995.

ZHR91
C. Zhou, C. A. R. Hoare, and A. P. Ravn. A calculus of durations. Information Processing Letters, 40:269-276, 1991.

Zub80
W. M. Zuberek. Timed Petri nets and preliminary performance evaluation. In Proceedings of the 7th Annual ACM Symposium on Computer Architecture, pages 88-96, 1980.

About this document ...

Strategic Directions in Computing Research
Concurrency Working Group Report

This document was generated using the LaTeX2HTML translator Version 96.1 (Feb 5, 1996) Copyright © 1993, 1994, 1995, 1996, Nikos Drakos, Computer Based Learning Unit, University of Leeds.

The command line arguments were:
latex2html -split 0 -link 0 -no_navigation -show_section_numbers final.tex.

The translation was initiated by Scott Smolka on Mon Sep 30 20:55:05 EDT 1996


Scott Smolka
Mon Sep 30 20:55:05 EDT 1996