Ohad Goudsmid, M.Sc. Thesis Seminar
Zoom Lecture: for link to zoom please contact firstname.lastname@example.org
Advisor: Prof. Orna Grumberg and Dr. Sarai Sheinvald
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.