Hyperproperties lift conventional trace properties in a way that describes how a system behaves in its entirety, and not just based on its individual traces, by allowing quantification over traces. Hyperproperties are very useful for describing security properties. Thus, performing hyperproperty model-checking is desired.

We generalize this notion to multi-properties, which describe the behavior of not just a single system, but of a set of systems, which we call a multi-model. We demonstrate the usefulness of our setting with practical examples. We show that model-checking multi-properties is equivalent to model-checking hyperproperties. However, our framework has the immediate advantage of being compositional, allowing to consider abstraction foreach component separately. 

We introduce sound and complete compositional proof rules for model-checking multi-properties, based on over- and under-approximations of the systems in the multi-model. We then describe methods of computing such approximations.  The first is abstraction-refinement based, in which a coarse initial abstraction is continually refined using counterexamples, until a suitable approximation is found. The second, tailored for models with finite traces, finds suitable approximations via the L^* learning algorithm.

We suggest improved algorithms for model-checking the ∀^∗∃^∗ fragment of both methods, which utilize additional information from the multi-property. Our methods can produce much smaller models than the original ones, and can therefore be used for accelerating model-checking for both multi-properties and hyperproperties.