arXiv:2310.02355

Reasoning about Intuitionistic Computation Tree Logic

Davide Catta, Vadim Malvone, Aniello Murano

제출 2023-10-03

원문 초록

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.

함께 살펴볼 논문

공통 태그를 근거로 연결했습니다. 실제 인용 관계나 논문의 우수성을 뜻하지 않습니다.

토론

이 논문과 연결된 포럼 글이 아직 없습니다.