A multiprocess network logic with temporal and spatial modalities

摘要

A modal logic which can be used to formally reason about synchronous fixed connection multiprocess networks such as of VLSI is introduced. The logic has both temporal and spatial modal operators. The various temporal 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. The spatial modal operators are useful to relate the properties of the current state of a given process with properties of the current state of neighboring processes. Many interesting properties of multiprocessor networks can be elegantly expressed in our logic. Examples of the diverse applications of the logic to packet routing, firing squad problems, systolic algorithms, and distributed system are given. Also some results in the decidability and complexity issues of this logic are presented.