Reducing the extensions of CTL with actions and real time

D.N. Jansen, Roelf J. Wieringa

Research output: Book/ReportReport

Abstract

In this report, we present the logic ATCTL, which combines two known extensions of CTL, namely ACTL and TCTL. ACTL extends CTL with constructs to describe actions and TCTL extends it with constructs to specify real-time properties. ATCTL combines both extensions. We use ATCTL as a language for property specification in which we can express state properties, action properties, and real-time properties. We show that the result can be reduced to ACTL as well as to TCTL, and therefore also to CTL. This makes model-checking ATCTL possible, because CTL model checkers exist.
LanguageUndefined
Place of PublicationEnschede
PublisherCentre for Telematics and Information Technology (CTIT)
Number of pages20
StatePublished - Dec 2000

Publication series

NameCTIT technical report series
PublisherUniversity of Twente, Centre for Telematics and Information Technology (CTIT)
No.TR-CTIT-00-27

Keywords

  • SCS-Services
  • METIS-119065
  • IR-56028
  • EWI-1667

Cite this

Jansen, D. N., & Wieringa, R. J. (2000). Reducing the extensions of CTL with actions and real time. (CTIT technical report series; No. TR-CTIT-00-27). Enschede: Centre for Telematics and Information Technology (CTIT).
Jansen, D.N. ; Wieringa, Roelf J./ Reducing the extensions of CTL with actions and real time. Enschede : Centre for Telematics and Information Technology (CTIT), 2000. 20 p. (CTIT technical report series; TR-CTIT-00-27).
@book{080f267788754ae6a446040517a91abe,
title = "Reducing the extensions of CTL with actions and real time",
abstract = "In this report, we present the logic ATCTL, which combines two known extensions of CTL, namely ACTL and TCTL. ACTL extends CTL with constructs to describe actions and TCTL extends it with constructs to specify real-time properties. ATCTL combines both extensions. We use ATCTL as a language for property specification in which we can express state properties, action properties, and real-time properties. We show that the result can be reduced to ACTL as well as to TCTL, and therefore also to CTL. This makes model-checking ATCTL possible, because CTL model checkers exist.",
keywords = "SCS-Services, METIS-119065, IR-56028, EWI-1667",
author = "D.N. Jansen and Wieringa, {Roelf J.}",
year = "2000",
month = "12",
language = "Undefined",
series = "CTIT technical report series",
publisher = "Centre for Telematics and Information Technology (CTIT)",
number = "TR-CTIT-00-27",
address = "Netherlands",

}

Jansen, DN & Wieringa, RJ 2000, Reducing the extensions of CTL with actions and real time. CTIT technical report series, no. TR-CTIT-00-27, Centre for Telematics and Information Technology (CTIT), Enschede.

Reducing the extensions of CTL with actions and real time. / Jansen, D.N.; Wieringa, Roelf J.

Enschede : Centre for Telematics and Information Technology (CTIT), 2000. 20 p. (CTIT technical report series; No. TR-CTIT-00-27).

Research output: Book/ReportReport

TY - BOOK

T1 - Reducing the extensions of CTL with actions and real time

AU - Jansen,D.N.

AU - Wieringa,Roelf J.

PY - 2000/12

Y1 - 2000/12

N2 - In this report, we present the logic ATCTL, which combines two known extensions of CTL, namely ACTL and TCTL. ACTL extends CTL with constructs to describe actions and TCTL extends it with constructs to specify real-time properties. ATCTL combines both extensions. We use ATCTL as a language for property specification in which we can express state properties, action properties, and real-time properties. We show that the result can be reduced to ACTL as well as to TCTL, and therefore also to CTL. This makes model-checking ATCTL possible, because CTL model checkers exist.

AB - In this report, we present the logic ATCTL, which combines two known extensions of CTL, namely ACTL and TCTL. ACTL extends CTL with constructs to describe actions and TCTL extends it with constructs to specify real-time properties. ATCTL combines both extensions. We use ATCTL as a language for property specification in which we can express state properties, action properties, and real-time properties. We show that the result can be reduced to ACTL as well as to TCTL, and therefore also to CTL. This makes model-checking ATCTL possible, because CTL model checkers exist.

KW - SCS-Services

KW - METIS-119065

KW - IR-56028

KW - EWI-1667

M3 - Report

T3 - CTIT technical report series

BT - Reducing the extensions of CTL with actions and real time

PB - Centre for Telematics and Information Technology (CTIT)

CY - Enschede

ER -

Jansen DN, Wieringa RJ. Reducing the extensions of CTL with actions and real time. Enschede: Centre for Telematics and Information Technology (CTIT), 2000. 20 p. (CTIT technical report series; TR-CTIT-00-27).