7
$\begingroup$

I am trying to trace back the origins of transition system semantics for imperative programs. I am assuming a transition system is a tuple $(\mathit{States}, \mathit{Trans})$ consisting of a set of states and a (binary) transition relation over states. By transition system semantics, I mean that there should be a mapping from programs to transition systems.

The presentation need not be exactly as I describe above and the mapping from programs to transition systems need not be completely explicit. For example, I would consider Plotkin's Structural Operational Semantics as providing transition system semantics to a formal language. Other early references I know of are due to Cousot & Cousot, and even earlier, due to Robert Keller in Formal Verification of Parallel Programs. There is earlier work by Richard Karp and Raymond Miller on reasoning about parallel programs, but their model is closer to Petri Nets and I am unsure about whether to read their paper as giving transition system semantics to programs.

Does anyone know of references from the early 80s or earlier where transition system semantics are provided for programs? Please add a few lines about the semantics and whether it is used today, and in what form.

$\endgroup$
7
$\begingroup$

Landin's SECD machine, originally described in The mechanical evaluation of expressions in 1964, is a transition system in the form of an abstract machine, later inspiring lots of of other abstract machines such as the CESK machine.

$\endgroup$
5
$\begingroup$
  1. There's Amir Pnueli's 1977 The Temporal Logic of Programs, where (as you doubtless know) the transition system is viewed as a Kripke frame. He cited the Keller paper you mention as his source of the idea that programs are transition systems. (I've never seen that one though.)

  2. Christopher Strachey gave semantics to stateful programs as state transformers on domains (i.e., a command is a partial function $S \to S_\bot$). This has an obvious reading as a transition function. This semantics is described in his amazing 1967 lecture notes Fundamental Concepts in Programming Languages.

$\endgroup$
  • $\begingroup$ Thanks. I did know Pnueli's paper. Strachey's notes look promising. $\endgroup$ – Vijay D Jul 23 '12 at 5:09
4
$\begingroup$

If you enlarge the idea of "programs" to include Turing machines, then the original Turing's description of their semantics was as transition systems. So, I think transition systems have always been with us!

$\endgroup$
  • $\begingroup$ Since biblical times? $\endgroup$ – Dave Clarke Jul 26 '12 at 20:41
  • $\begingroup$ @Dave Clarke. Well, I can't say. Even though algorithms have always been written in an imperative style (long before biblical times!), they were designed for humans to execute with pencil and paper and, so, didn't involve genuine state change. Turing seems to have been the first one. I don't know if he realized how big a step he was taking by writing a new bit into a tape cell overwriting an old bit. Perhaps he did! $\endgroup$ – Uday Reddy Jul 26 '12 at 22:38
1
$\begingroup$

Go read Knuth, The Art of Computer Programming, where he gives definitions similar to what you mention. It appears that he gives exactly one reference, namely to a book by A. A. Markov from 1951 called Theory of Algorithms. This may or may not be what you want.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.