LPrL: An Asynchronous Linear Time Hyper Logic

TL;DR

This paper introduces LPrL, an asynchronous hyper linear time temporal logic extending LTL with first-order features, enabling decidable satisfiability and model checking, unlike the undecidable HyperLTL.

Contribution

The paper proposes LPrL, a new asynchronous hyper linear time logic with first-order extension, and proves its satisfiability and model checking are decidable in elementary time.

Findings

LPrL can express security policies and distributed process properties.

Satisfiability and model checking for LPrL are decidable in elementary time.

Contrasts with HyperLTL, which has undecidable satisfiability and non-elementary model checking complexity.

Abstract

We present a novel asynchronous hyper linear time temporal logic named LPrL (Linear Time Predicate Logic) and establish its basic theory. LPrL is a natural first order extension of LTL (Linear time temporal logic), in which the predicates specify the properties of and the relationships between traces (infinite sequences of actions) using Boolean combinations of LTL formulas. To augment the expressive power of the logic, we introduce a simple language of terms and add the equality predicate t = t' where t and t' are terms. We first illustrate how a number of the security policies as well as a basic consistency property of distributed processes can be captured using LPrL. We then establish our main results using automata theoretic techniques. Namely, the satisfiability and model checking problems for LPrL can be solved in elementary time. These results are in sharp contrast to HyperLTL, the prevalent synchronous hyper linear time logic, whose satisfiability problem is undecidable and whose model checking problem has non-elementary time complexity.