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.

Machine aided computation for system validation and verification

Validation: by simulation and testing (only partially explore the possible states)

Verification: by theorem proof, formula rewriting, prove checker, model checking. The common feature is that these techniques consider all the behavior of a system. Model checking is a little bit similar to validation as it explores all the possible trajectories of a system, but with symbolic algorithms.

Celebrate Chinese New Year

Today is New Year’s eve for Chinese New Year (a pig year). I phoned my mother in China. After leaving China for almost 10 years, this is the first time I felt lonely. For all the past, I was so attracted by my new life and my freedom. I was curious on many things. Now I feel the older generation is getting old and more responsibilities are on my shoulder. But I am still very far away and cannot go home in this season. A little bit sad.

Here is the lyric of a song written by Ray Conniff. He was inspired by the Lara’s theme (composed by Maurice Jarre) in the movie Dr. Zhivago (1965, directed by David Lean). I watched this movie in the summer of 1988, when the political atmosphere was loose in China. I was moved by this movie and read the novel later. It is interesting that all the books are actually available in China, just what you choose to believe.

Devote this to my family and my beloved friends.

Somewhere, my love

Somewhere, my love,
There will be songs to sing
Although the snow
Covers the hope of spring.

Somewhere a hill
Blossoms in green and gold
And there are dreams
All that your heart can hold.

Someday we'll meet again, my love.
Someday whenever the spring breaks through.

You'll come to me
Out of the long ago,
Warm as the wind,
Soft as the kiss of snow.

Till then, my sweet,
Think of me now and then.
God, speed my love
'Til you are mine again.