On interval dynamic logic: Introducing quasi-action lattices

Abstract

In this paper we discuss the incompatibility between the notions of validity and impreciseness in the context of Dynamic Logics. To achieve that we consider the Łukasiewicz action lattice and its interval counterpart, we show how some validities fail in the context of intervals. In order to capture the properties of action lattices that remain valid for intervals we propose a new structure called Quasi-action Lattices which generalizes action lattices and is able to model both: The Łukasiewicz action lattice, Ł, and its interval counterpart, Łˆ. The notion of graded satisfaction relation is extended to quasi-action lattices. We demonstrate that, in the case of intervals, the relation of graded satisfaction is correct (cf. Theorem 3) with respect to the graded satisfaction relation on the Łukasiewicz action lattice. Although this theorem guarantees that satisfiability is preserved on intervals, we show that validity is not. We propose, then, to weaken the notion of validity on action lattices to designated validity on quasi-action lattices. In this context, Theorem 4 guarantees that the dynamic formulæ which are valid with respect to Ł will be designated valid with respect to Łˆ