Concurrency

Classic automaton, which is the theoretical foundation of CS, does not have semantics for concurrency. Other formal models, such as Petri net and Process Algebra, do. Concurrency brings state explosion problem is we want to enumerate all the reachable states of a system. The number of the states may be exponential to the size of the nodes.

I am thinking how many formal models I know that can represent concurrency and what are the common computation techniques for concurrency.

Concurrent Automaton: is a finite automaton. Its state set consists of reachable marking of a Petri net. Its labels are semiorders (the sequence of transitions on optional branches, concurrent branches are a piece of semiorder).

Abstract State Machine (ASM, see my post on Dec. 16, 2006): the state is arbitrary data structure, the transitions are guarded and can be fired concurrently from a state.

Web Service Interface (by Beyer, Chakrabarti and Henzin): based on Interface Automaton (de Algaro, Henzinger). The concurrent branches can be represented by operators, proof rules (semantic operations) to define how to reason about the algebra.