Skip to content (access key 's')
Logo of Technion
Logo of CS Department

The Taub Faculty of Computer Science Events and Talks

Compositional Model Checking for Multi-Properties
event speaker icon
Ohad Goudsmid (M.Sc. Thesis Seminar)
event date icon
Sunday, 24.01.2021, 15:30
event location icon
Zoom Lecture: for link to zoom please contact
event speaker icon
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.