On the Approximation Relation on Dynamic Logic Models

Vladimir A. Zakharov

We deal with the equivalence problem for deterministic propositional sequential programs whose semantics is defined by means of dynamic logic models. Let A and P be the alphabets of basic actions and propositional variables. A sequential program π over A and P is a finite transition system whose nodes are associated with basic actions and transitions are labelled by formulae built of propositional variables by means of connectives ¬ and ∧. Dynamic logic models over A and P are defined as in [1]. We assume that some initial state s_{0} is distinguished in every model σ. The run π(σ) of a program π on a model σ is defined as usual (see [2]). If π(σ) terminates and reaches some state s in σ then the result [π(σ)] of this run is s; otherwise [π(σ)] is undefined. By a semantics we mean any set M of dynamic logic models. If all models in M are based on the same frame F then M is called a homogeneous semantics. Programs π_{1} and π_{2} are called equivalent on M (π_{1} ∼_{M} π_{2} in symbols) iff [π_{1}(σ)] = [π_{2}(σ)] holds for each model σ in M. We say that a semantics M_{1} approximates semantics M_{2} (M_{2} ⪯ M_{1}) iff π_{1} ∼_{M_{1}} π_{2} implies π_{1} ∼_{M_{2}} π_{2} for every pair of programs π_{1}, π_{2}. If both M_{2} ⪯ M_{1} and M_{1} ⪯ M_{2} hold then we write M_{1} ≈ M_{2}. A semantics M is called saturated iff M ≉ M ∪ {σ} holds for every model σ which is not in M. A homogeneous semantics M based on a frame F is called homogeneously saturated iff M ≉ M ∪ {σ} holds for every model σ based on F which is not in M. We study the lattice-theoretic properties of semantics w.r.t. approximation relation ⪯. Denote by AP (M_{1}, M_{2}) the following assertion: each model σ_{2} in M_{2} is a homomorphic image of some model σ_{1} in M_{1}. Clearly, AP (M_{1}, M_{2}) implies M_{2} ⪯ M_{1} for arbitrary semantics. Proposition 1. Suppose M_{1} and M_{2} are saturated semantics. Then M_{2} ⪯ M_{1} iff AP (M_{1}, M_{2}) holds. Corollary 1. The set of saturated semantics is a complete lattice w.r.t. ⪯. Proposition 2. There exists a pair M_{1}, M_{2} of homogeneously saturated semantics such that M_{2} ⪯ M_{1} but AP (M_{1}, M_{2}) does not hold. Corollary 2. The set of homogeneously saturated semantics is a lower semi-lattice but not a lattice. Corollary 3. There exists a saturated semantics M which has not the least homogeneous approximation.

[1] Harel D., Dynamic logics // Handbook of Philosophical Logics, D.Gabbay and F.Guenthner (eds.), 1984, p.497-604.

[2] Zakharov V.A. An efficient and unified approach to the decidability of equivalence of propositional programs // Lecture Notes in Computer Science, 1998, 1443, p.247-259.

Address: Faculty of Computational Mathematics and Cybernetics, Moscow State University, Moscow, RU-119899, Russia

E-mail: zakh@cs.msu.su