Synthesis of Communicating Process Skeletons from Temporal-Spatial Logic Specifications

Temporal-spatial logic is a propositional logic with temporal and spatial modalities asserting on a network. In this paper, a tableau-like decision procedure for network satisfiability in that logic is presented and used in the synthesis of communicating skeletons of CSP-like programs. By explicitly introducing communication network in the logic system, our approach has some advantages over the temporal one.