A multiprocess network logic with temporal and spatial modalities

Published

Journal Article

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.

Full Text

Duke Authors

Cited Authors

  • Reif, J; Sistla, AP

Published Date

  • January 1, 1985

Published In

Volume / Issue

  • 30 / 1

Start / End Page

  • 41 - 53

Electronic International Standard Serial Number (EISSN)

  • 1090-2724

International Standard Serial Number (ISSN)

  • 0022-0000

Digital Object Identifier (DOI)

  • 10.1016/0022-0000(85)90003-0

Citation Source

  • Scopus