Technical Report MSC-2021-11

TR#:MSC-2021-11
Class:MSC
Title: Compositional Model-Checking for Multi-Properties
Authors: Ohad Goudsmid
Supervisors: Orna Grumberg, Sarai Sheinvald
PDFCurrently accessibly only within the Technion network
Abstract: 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 for each 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 $\forall^*\exists^*$ 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.

CopyrightThe above paper is copyright by the Technion, Author(s), or others. Please contact the author(s) for more information

Remark: Any link to this technical report should be to this page (http://www.cs.technion.ac.il/users/wwwb/cgi-bin/tr-info.cgi/2021/MSC/MSC-2021-11), rather than to the URL of the PDF files directly. The latter URLs may change without notice.

To the list of the MSC technical reports of 2021
To the main CS technical reports page

Computer science department, Technion
admin