Reasoning about Intuitionistic Computation Tree Logic

TL;DR

This paper introduces an intuitionistic variant of Computation Tree Logic (CTL), exploring its semantics, syntax, and properties, and highlighting differences from classical CTL such as the invalidity of certain fixed-point axioms.

Contribution

It defines and analyzes an intuitionistic version of CTL, providing new insights into its semantic features and logical properties for formal verification.

Findings

Some fixed-point axioms of classical CTL are invalid in the intuitionistic version

The intuitionistic CTL has distinct semantic characteristics from classical CTL

Basic properties of the intuitionistic CTL are studied and discussed

Abstract

In this paper, we define an intuitionistic version of Computation Tree Logic. After explaining the semantic features of intuitionistic logic, we examine how these characteristics can be interesting for formal verification purposes. Subsequently, we define the syntax and semantics of our intuitionistic version of CTL and study some simple properties of the so obtained logic. We conclude by demonstrating that some fixed-point axioms of CTL are not valid in the intuitionistic version of CTL we have defined.