Propositional dynamic logic in two- and more dimensions
pp. 323-329
in: Dimiter G. Skordev (ed), Mathematical logic and its applications, Berlin, Springer, 1987Abstract
The Propositional Dynamic Logic PDL extends the Kripke modal logic with the intension to frame the behavior and formalize the properties of computer programs. A program α(as a rule non-deterministic) and a property A are interpreted respectively as a binary relation R(α) and a subset V(A) of some presupposed universe U={u, v, …}. Its elements are refered to as possible worlds or memory states and are traditionally regarded as some indivisible units. The aim of this paper is to suggest a reliable framework and to establish some basic results for that case, where the memory states have themselves been divided and granted the structure of ordered pairs (or generally, ordered N-tuples). In this case, formally R(α) and V(A) will be quaternary and binary relations, respectively. Informally this corresponds to the case of computation with two-cell memory device.