• Kripke
• logica modale quantificata
• quantified modal logic
• counterpart
• formula in context

We propose a predicative modal logic of the second order for expressing properties of the evolution of software systems. Each state of a system is specified as a unary algebra, and our logics allows to formalize the problem of verifying the properties of system evolutions as the checking of the truth of suitable formulas. The level of abstraction guaranteed by the algebraic presentation of system states allows the unification of many proposals in the literature, at the same time obtaining a greater level of expressiveness in terms of system representability.
Due to a different handling of the so-called “trans-world identity”, we consider two alternative semantics for our logic: a “Kripke-like” model and a “Counterpart-like” one. Furthermore, we instantiate our proposal by considering unary algebras representing graphs, thus showing the applicability of our approach to the graph transformation framework.