Algorithms for CTL system modification

Yulin Ding; Yan Zhang; Robert J. Howlett; Lakhmi C. Jain; Rajiv Khosla

Algorithms for CTL system modification

Yulin Ding, Yan Zhang, Robert J. Howlett, Lakhmi C. Jain, Rajiv Khosla

School of Computer, Data & Mathematical Sciences

Research output: Chapter in Book / Conference Paper › Conference Paper

Abstract

Model updating, as a new concept to be employed as a standard and universal method for system modification, has been started in and further developed in this paper. This paper introduces algorithms for Computation Tree Logic (CTL) model update. The algorithms correct errors in a CTL Kripke model to make this model satisfy its various required properties. These update algorithms are designed through pseudo-code, which details the logic of the algorithms. The microwave oven example in has been correctly treated by the pseudo-code, which demonstrates the feasibility of these algorithms. The algorithms and their pseudo-code are the foundations for later implementation of a CTL model updater and integration of a CTL model checker and this updater.

Original language	English
Title of host publication	9th International Conference, KES 2005, Melbourne, Australia, September 14-16, 2005 : Proceedings, Part I
Publisher	Springer
Number of pages	7
ISBN (Print)	9783540319832
Publication status	Published - 2005
Event	International Conference on Knowledge-Based Intelligent Information and Engineering Systems - Duration: 8 Sept 2010 → …

Conference

Conference	International Conference on Knowledge-Based Intelligent Information and Engineering Systems
Period	8/09/10 → …

Keywords

computer systems
system modification
computation tree logic (CTL)
model checking
algorithms

Cite this

@inproceedings{40caa971c03b454bb286498cfcde1d73,

title = "Algorithms for CTL system modification",

abstract = "Model updating, as a new concept to be employed as a standard and universal method for system modification, has been started in and further developed in this paper. This paper introduces algorithms for Computation Tree Logic (CTL) model update. The algorithms correct errors in a CTL Kripke model to make this model satisfy its various required properties. These update algorithms are designed through pseudo-code, which details the logic of the algorithms. The microwave oven example in has been correctly treated by the pseudo-code, which demonstrates the feasibility of these algorithms. The algorithms and their pseudo-code are the foundations for later implementation of a CTL model updater and integration of a CTL model checker and this updater.",

keywords = "computer systems, system modification, computation tree logic (CTL), model checking, algorithms",

author = "Yulin Ding and Yan Zhang and Howlett, {Robert J.} and Jain, {Lakhmi C.} and Rajiv Khosla",

year = "2005",

language = "English",

isbn = "9783540319832",

booktitle = "9th International Conference, KES 2005, Melbourne, Australia, September 14-16, 2005 : Proceedings, Part I",

publisher = "Springer",

note = "International Conference on Knowledge-Based Intelligent Information and Engineering Systems ; Conference date: 08-09-2010",

}

TY - GEN

T1 - Algorithms for CTL system modification

AU - Ding, Yulin

AU - Zhang, Yan

AU - Howlett, Robert J.

AU - Jain, Lakhmi C.

AU - Khosla, Rajiv

PY - 2005

Y1 - 2005

N2 - Model updating, as a new concept to be employed as a standard and universal method for system modification, has been started in and further developed in this paper. This paper introduces algorithms for Computation Tree Logic (CTL) model update. The algorithms correct errors in a CTL Kripke model to make this model satisfy its various required properties. These update algorithms are designed through pseudo-code, which details the logic of the algorithms. The microwave oven example in has been correctly treated by the pseudo-code, which demonstrates the feasibility of these algorithms. The algorithms and their pseudo-code are the foundations for later implementation of a CTL model updater and integration of a CTL model checker and this updater.

AB - Model updating, as a new concept to be employed as a standard and universal method for system modification, has been started in and further developed in this paper. This paper introduces algorithms for Computation Tree Logic (CTL) model update. The algorithms correct errors in a CTL Kripke model to make this model satisfy its various required properties. These update algorithms are designed through pseudo-code, which details the logic of the algorithms. The microwave oven example in has been correctly treated by the pseudo-code, which demonstrates the feasibility of these algorithms. The algorithms and their pseudo-code are the foundations for later implementation of a CTL model updater and integration of a CTL model checker and this updater.

KW - computer systems

KW - system modification

KW - computation tree logic (CTL)

KW - model checking

KW - algorithms

UR - http://handle.uws.edu.au:8081/1959.7/40560

M3 - Conference Paper

SN - 9783540319832

BT - 9th International Conference, KES 2005, Melbourne, Australia, September 14-16, 2005 : Proceedings, Part I

PB - Springer

T2 - International Conference on Knowledge-Based Intelligent Information and Engineering Systems

Y2 - 8 September 2010

ER -

Algorithms for CTL system modification

Abstract

Conference

Keywords

Other files and links

Fingerprint

Cite this