  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.
