Proving Temporal Properties of Z Specifications Using Abstraction

This paper presents a systematic approach to proving temporal properties of arbitrary Z specifications. The approach involves (i) transforming the Z specification to an abstract temporal structure (or state transition system), (ii) applying a model checker to the temporal structure, (iii) determining whether the temporal structure is too abstract based on the model checking result and (iv) refining the temporal structure where necessary. The approach is based on existing work from the model checking literature, adapting it to Z.

Algebraic Bethe ansatz for integrable extended Hubbard models arising from supersymmetric group solutions

Integrable extended Hubbard models arising from symmetric group solutions are examined in the framework of the graded quantum inverse scattering method. The Bethe ansatz equations for all these models are derived by using the algebraic Bethe ansatz method.