Hyperproperties in Matching Logic

Abstract

Matching logic is a uniform logic to specify and reason about programming languages and program properties. Many important logics and/or formal systems have been shown to be definable in matching logic as logical theories. However, no research has been conducted to studying how hyperproperties can be treated in matching logic. In this paper, we give the first theoretical result that shows that HyperLTL (hyper linear temporal logic), which is an important temporal logic designed for specifying and reasoning about hyperproperties, can be completely captured by matching logic. Our result demonstrates that matching logic offers a uniform treatment to handling hyperproperties and to supporting their model checking problems.