A dynamic logic of multiprocessing with incomplete information
A crucial property of distributed multiprocessing systems is the lack of complete information by any given process about the states of other processes. The contribution of this paper is a fundamental modal logic, MPL, for multiprocessing with incomplete information. (Section 1.5 gives an informal introduction to MPL; the formal definitions are in Section 2.) By way of this logic, we develop a solid (practical and theoretical) correspondence between distributed multiprocessing and multiplayer games of incomplete information. Fischer and Ladner, [1979] have shown a logspace reduction from the outcome problem for two person games of perfect information to satisfiability of formulas in their propositional dynamic logic (PDL). We provide in Section 3 a log-space reduction from the outcome problem for multiplayer games of incomplete information to satisfiability of formulas in our logic MPL. Although in general satisfiability in out logic is undecidable, the satisfiability problem of formulae with hierarchical visibility structure is shown decidable (using the methods for solving hierarchical games developed in Reif [1979] and Peterson and Reif [1979], and also the model theoretic techniques of Fischer and Ladner [1979] and Pratt [1979b]). At a more practical level, we argue that the game-like semantics of our logic provides a robust paradigm in which to view distributed multiprocessing problems. We apply our logic to describe total correctness properties of multi-process programs with shared variables as well as communicating processes with "handshake"-type message passing.
