Synthesis of communicating process skeletons from temporal-spatial logic specifications (Q1116944)

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 a communication network in the logic system, our approach has some advantages over the temporal one.