Reasoning about Intuitionistic Computation Tree Logic
This work addresses formal verification challenges for researchers in logic and computer science, but it is incremental as it adapts an existing logic framework.
The paper tackles the problem of defining an intuitionistic version of Computation Tree Logic (CTL) for formal verification, resulting in the demonstration that some fixed-point axioms of CTL are not valid in this new logic.
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.