Compositional Model Checking for Multi-Properties
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 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. 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 continuously 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.
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.
Sun 17 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
17:00 - 17:30
|Compositional Model Checking for Multi-Properties|
Ohad Goudsmid Department of Computer Science, The Technion, Orna Grumberg Technion – Israel Institute of Technology, Sarai Sheinvald Department of Software Engineering, ORT Braude College of EngineeringMedia Attached
|Decomposing Data Structure Commutativity Proofs with mn-Differencing|