Reasoning about Dynamic Features in Specification Languages. A Modal view on Creation and Modification

Using algebras over some signature to model the notion of state is quite common in specification languages. Some specification formalisms, e.g. COLD and Evolving Algebras, also allow for the dynamic change of states. Two kinds of elementary procedures are used: creation (of a new object) and modification (of a function or predicate at some point). In this paper we present and investigate MLCM (Modal Logic of Creation and Modification), a multimodal predicate logic for reasoning over programs built up from such procedures. MLCM deviates from traditional dynamic predicate logic in two respects: creation is added as a primitive program construct and assignment (to variables) is replaced by assignment to constants and parametrized assignment to function and predicate symbols. We present a definition of syntax, semantics and axiomatisation of MLCM and establish completeness for the repetition-free fragment via a traditional Henkin construction.