The Taub Faculty of Computer Science Events and Talks

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. We generalize this notion to multi-properties, which describe the behavior of a set of systems, called a multi-model. We show that model-checking multi-properties is equivalent to model-checking hyperproperties. We introduce sound and complete compositional proof rules for model-checking multiproperties, based on approximations of the systems in the multi-model and describe methods of computing them. 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.