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

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 goudsmidohad@cs.technion.ac.il
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.