A multiprocess network logic with temporal and spatial modalities
type: Item
instance of: scholarly article
title: A multiprocess network logic with temporal and spatial modalities
zbMATH Open document ID: 0565.68031
DOI: 10.1016/0022-0000(85)90003-0
author: A. P. Sistla
author: J. Reif
published in: Journal of Computer and System Sciences
publication date: 1985-01-01T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 68Q65
Mathematics Subject Classification ID: 03B45
zbMATH DE Number: 3902024
zbMATH Keywords: temporal modalities
zbMATH Keywords: spatial modalities
zbMATH Keywords: computations on networks with complex connections
zbMATH Keywords: multidimensional temporal logic
zbMATH Keywords: syntax
zbMATH Keywords: semantics
zbMATH Keywords: routing on a shuffle-exchange network
zbMATH Keywords: firing squad problem for a linear array
zbMATH Keywords: systolic arithmetic computations
zbMATH Keywords: distributed systems
zbMATH Keywords: decidability
zbMATH Keywords: complexity
reviewed by: Satoshi Miura
MaRDI profile type: Publication
full work available at URL: 0022-0000(85)90003-0
OpenAlex ID: W2019539243
cites work: The temporal logic of branching time
cites work: Q3336675
cites work: Real-Time Computation by n-Dimensional Iterative Arrays of Finite-State Machines
cites work: Propositional dynamic logic of regular programs
cites work: The propositional dynamic logic of deterministic, well-structured programs
cites work: Formalization of Properties of Functional Programs
cites work: Q3746875
cites work: Relationships between nondeterministic and deterministic tape complexities
cites work: Ultracomputers
cites work: The complexity of propositional linear temporal logics
cites work: Parallel Processing with the Perfect Shuffle
Recommended article: A model and temporal proof system for networks of processes
Recommended article: SpaTeL
Recommended article: Frontiers of Combining Systems
Recommended article: Q3347282
Recommended article: Q4536331
Recommended article: Multi-dimensional modal logic as a framework for spatio-temporal reasoning
Recommended article: Q4702960
Recommended article: Q3341874
Recommended article: A Temporal Logic for Multi-threaded Programs
Recommended article: Modal and temporal logics for abstract space-time structures
description: scientific article; zbMATH DE number 3902024