Space State Topologies and a Theory of Convergence for Temporal Logics
by
Norm Howes
Institute for Defense Analyses

We describe a logic for discussing the behavior of computer systems. Within this logic we can define concepts, state axioms, and prove theorems about the behavior of computer systems. One of the concepts we define is the topology of the state space of the computer system under discussion. The introduction of a topology on the space of states in which the system can exist gives rise to the concept of limit states to which behaviors of the system can converge. We use the definition of behavior from the Temporal Logic of Actions (TLA). A behavior is a sequence of states and computer systems are characterized by their set of possible behaviors. In order to topologize state space we define state space differently than in TLA and introduce an extension of TLA that we call TLB to designate the Temporal Logic of Behaviors. We introduce new temporal operators that characterize the concepts of converging and clustering and discuss the possibility of extending existing automated temporal formula verifiers to include these new operators. The advantage of TLB over TLA is something like the advantage of calculus over algebra. Traditional questions about correctness, liveness, safety, etc. can be proved within TLA without the concept of a limit state. But for higher levels of system abstraction, such as at the application level, we may be interested in investigating whether algorithms converge to specific states. For this type of investigation we need the concept of a limit point.

Date received: March 19, 2002