A multiprocess network logic with temporal and spatial modalities (Q1058846)

This paper proposes a formal logic allowing use of both temporal and spatial modal operators, such as nexttime, eventually, hereafter, untill, somewhere, everywhere, in the context of a fixed connection network. The various temporal (spatial) modal operators can be used to relate the properties of the current state of a given process with properties of succeeding states of the same process (of current state of neighboring processes). This combination of temporal and spatial modal operators allows us to formally reason about computations on networks with complex connections. Indeed, one can view this logic as multidimensional temporal logic. Section 2 defines the logic: syntax, networks, semantics, where a model \({\mathcal M}\) is defined in a different way which is more in the style of propositional dynamic logic of structures, and extensions to a first order logic. Section 3 describes applications of the logic: routing on a shuffle-exchange network, the firing squad problem for a linear array, systolic arithmetic computations, and expressing some properties in distributed systems. Section 4 investigates issues of decidability and complexity of different versions of the logic.