Michael Jones, PhD

It is accepted that there are no good functional models of concurrency. A functional model maps inputs to outputs. Concurrency models begin with a definition of an atomic action. All models use atomic actions and differ in how they "capture the notion of system execution." There are "automata-based" which descibe concurrent systems as "states and transitions between states" and there are "action-based" models which model systems using "structures consisting of atomic actions." An early action-based model was trace theory.

Intensional models "require explicit description of system states and possible state changes" Extensional models "concentrate on the pattern of possible interactions over time".

Interleaving models assume that "observations of system behavior are sequential" so that "parallel actions [are] reduced to nondeterministic interleaving." Truly concurrent models "treat concurrency as fundamental" and system behavior is "represented in terms of the causal relations among events performed by the components of distributed states"

Then there's branching v. linear time. Branching time allows one to track when computational paths diverge.

Either use logical formulas to describe concurrent systems or use an abstract concurrent system to describe the correct concurrent system. Logics are available for branching and linear time specification of correctness (in the form of LTL and CTL, as might be expected). But the differences between interleaved and truly concurrent models remains undeveloped as do the differences between intensional and extensional views of system behavior.

I think our most useful model would be an intentional model that uses interleaved semantics and a branching model of time.

van Glabbeek gives 5 convenient classes of concurrency models.

1. graph: like an automata based model.
   
2. net: like petri nets.
   
3. event: a set of events with "some structure on" the set of events that "determines the relations between events" Reminds me of Smolka's intentional models.
   
4. explicit: looks like what Smolka would call a "specification using a system to specify a more concrete system"
   
5. term like CSP or CCS a language with a syntax and a semantics.