New predicate transformer for symbolic modeling

ABSTRACT. The paper presents new predicate transformer for symbolic modeling. Predicate transformer is a symbolic function that is used for computing transitions of a system with states represented by means of first-order formulas. Systems under consideration are compositions of environments and agents inserted into these environments (insertion models). They are specified by means of basic protocols, which represent formal requirements to systems. Previous version of predicate transformer allowed only existential quantifiers in formulas. A new one allows both quantifiers but with some restriction on formulas. The use of universal quantifier is illustrated on the example of MESI protocol.