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. © 1985.
Duke Scholars
Published In
DOI
EISSN
ISSN
Publication Date
Volume
Issue
Start / End Page
Related Subject Headings
- Computation Theory & Mathematics
- 49 Mathematical sciences
- 46 Information and computing sciences
- 0806 Information Systems
- 0805 Distributed Computing
- 0802 Computation Theory and Mathematics
Citation
Published In
DOI
EISSN
ISSN
Publication Date
Volume
Issue
Start / End Page
Related Subject Headings
- Computation Theory & Mathematics
- 49 Mathematical sciences
- 46 Information and computing sciences
- 0806 Information Systems
- 0805 Distributed Computing
- 0802 Computation Theory and Mathematics