University of Illinois Urbana-Champaign

Hyperproperties in Matching Logic

Tusil, Jan; Chen, Xiaohong; Rosu, Grigore

Content Files
tusil-chen-rosu-2021-tr.pdf

Permalink

https://hdl.handle.net/2142/109298

Description

Title
Hyperproperties in Matching Logic
Author(s)
  • Tusil, Jan
  • Chen, Xiaohong
  • Rosu, Grigore
Issue Date
2021
Keyword(s)
  • hyperproperties
  • matching logic
Date of Ingest
2021-02-19T15:20:53Z
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.
Type of Resource
text
Genre of Resource
technical report
Language
en
Permalink
http://hdl.handle.net/2142/109298

Owning Collections

Research and Tech Reports - Computer Science PRIMARY