Reasoning about Intuitionistic Computation Tree Logic

Davide Catta; Vadim Malvone; Aniello Murano

doi:10.4204/EPTCS.391.6

Reasoning about Intuitionistic Computation Tree Logic

Davide Catta
, Vadim Malvone
, Aniello Murano

University of Naples Federico II

Résultats de recherche: Contribution à un journal › Article de conférence › Revue par des pairs

Résumé

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.

langue originale	Anglais
Pages (de - à)	42-48
Nombre de pages	7
journal	Electronic Proceedings in Theoretical Computer Science, EPTCS
Volume	391
Les DOIs	https://doi.org/10.4204/EPTCS.391.6
état	Publié - 30 sept. 2023
Evénement	3rd Workshop on Agents and Robots for Reliable Engineered Autonomy, AREA 2023 - Krakow, Pologne Durée: 1 oct. 2023 → …

Accès au document

10.4204/EPTCS.391.6

Autres fichiers et liens

Lien vers la publication dans Scopus

Contient cette citation

@article{b3475edd1caa40dc90e68c3e350e6f2f,

title = "Reasoning about Intuitionistic Computation Tree Logic",

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.",

author = "Davide Catta and Vadim Malvone and Aniello Murano",

note = "Publisher Copyright: {\textcopyright} D. Catta, V. Malvone \& A. Murano.; 3rd Workshop on Agents and Robots for Reliable Engineered Autonomy, AREA 2023 ; Conference date: 01-10-2023",

year = "2023",

month = sep,

day = "30",

doi = "10.4204/EPTCS.391.6",

language = "English",

volume = "391",

pages = "42--48",

journal = "Electronic Proceedings in Theoretical Computer Science, EPTCS",

issn = "2075-2180",

}

TY - JOUR

T1 - Reasoning about Intuitionistic Computation Tree Logic

AU - Catta, Davide

AU - Malvone, Vadim

AU - Murano, Aniello

N1 - Publisher Copyright: © D. Catta, V. Malvone & A. Murano.

PY - 2023/9/30

Y1 - 2023/9/30

N2 - 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.

AB - 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.

UR - https://www.scopus.com/pages/publications/85174826027

U2 - 10.4204/EPTCS.391.6

DO - 10.4204/EPTCS.391.6

M3 - Conference article

AN - SCOPUS:85174826027

SN - 2075-2180

VL - 391

SP - 42

EP - 48

JO - Electronic Proceedings in Theoretical Computer Science, EPTCS

JF - Electronic Proceedings in Theoretical Computer Science, EPTCS

T2 - 3rd Workshop on Agents and Robots for Reliable Engineered Autonomy, AREA 2023

Y2 - 1 October 2023

ER -

Reasoning about Intuitionistic Computation Tree Logic

Résumé

Accès au document

Autres fichiers et liens

Empreinte digitale

Contient cette citation