On the Expressive Power of the Normal Form for Branching-Time Temporal Logics

TL;DR

This paper explores the expressive capabilities of the branching-time normal form (BNF) in temporal logics, demonstrating its ability to encode automata and facilitate verification through deductive reasoning techniques.

Contribution

It introduces BNF as a high-level normal form for branching-time temporal logics, enabling automata encoding and improved verification methods.

Findings

BNF can encode Buchi Tree Automata.

BNF allows translation of specifications into a form suitable for deductive verification.

The approach facilitates extracting hidden invariants in complex temporal specifications.

Abstract

With the emerging applications that involve complex distributed systems branching-time specifications are specifically important as they reflect dynamic and non-deterministic nature of such applications. We describe the expressive power of a simple yet powerful branching-time specification framework -- branching-time normal form (BNF), which has been developed as part of clausal resolution for branching-time temporal logics. We show the encoding of Buchi Tree Automata in the language of the normal form, thus representing, syntactically, tree automata in a high-level way. Thus we can treat BNF as a normal form for the latter. These results enable us (1) to translate given problem specifications into the normal form and apply as a verification method a deductive reasoning technique -- the clausal temporal resolution; (2) to apply one of the core components of the resolution method -- the loop searching to extract, syntactically, hidden invariants in a wide range of complex temporal specifications.