Reducing the extensions of CTL with actions and real time

D.N. Jansen; Roelf J. Wieringa

Reducing the extensions of CTL with actions and real time

D.N. Jansen, Roelf J. Wieringa

Research output: Book/Report › Report › Professional

80 Downloads (Pure)

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.

Original language	Undefined
Place of Publication	Enschede
Publisher	Centre for Telematics and Information Technology (CTIT)
Number of pages	20
Publication status	Published - Dec 2000

Publication series

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

Keywords

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

Access to Document

http://purl.org/utwente/18545

Cite this

@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 = dec,

language = "Undefined",

series = "CTIT technical report series",

publisher = "Centre for Telematics and Information Technology (CTIT)",

number = "TR-CTIT-00-27",

address = "Netherlands",

}

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 -