Comparing some Intuitions of 'Process Calculus' and 'Program Logic'

摘要

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.