Journal of Logic and Computation, Volume 11, Issue 6, pp. 789-827: Abstract.
Comparing some Intuitions of `Process Calculus' and `Program Logic'
Department of Computer Science, University of Essex, Colchester CO4 3SQ. E-mail: email@example.com
Suppose one needs to reason about about evolving systems such as programs or agents. One standard tradition (the `event-and-order tradition') describes what the system does as a tree of possible events, with forks as choices or discoveries. Process calculus is a typical version. Another tradition (the `state-and-time tradition') describes what the system does as a set of alternative histories (sequences of states) that the system can drive the world through as it acts. Dynamic and temporal logics are typical versions. One contribution of this paper is an account of how a process seen as a tree in the event-and-order tradition can be understood as an abstraction of a process seen as a set of alternative histories in the state-and-time tradition. The abstraction can be formalized as two equivalence relations, one between states on a single history, which describe the edges in the process seen as a tree, and one between states on different histories, which describes the forking in the process seen as a tree. It is shown that exactly what such an abstraction omits is information about which points in two separate processes seen as trees can be reached together. However, the paper arose from the author's difficulty in understanding which tradition was more appropriate for a particular area of artificial intelligence. Because of that, the paper also contrasts some of the intuitions behind the traditions about how to describe the world.
Keywords: Process calculus, program logic, state, event, choice, observation, action