Model updating CTL systems

Yulin Ding; Yan Zhang; Ray Jarvis; Shichao Zhang

Model updating CTL systems

Yulin Ding
, Yan Zhang
, Ray Jarvis
, Shichao Zhang

School of Computer, Data & Mathematical Sciences

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

Abstract

Minimal change is a fundamental principle for modelling system dynamics. In this paper, we study the issue of minimal change for Computational Tree Logic (CTL) model update. We first consider five primitive updates which capture the basic update operations in the CTL model. Based on these primitive updates, we then define the minimal change criteria for CTL model update and develop formal algorithms that embed the underlying minimal change principle. We also present the well known microwave oven scenario to demonstrate our update algorithms. Our work presented in this paper can be viewed as the first formalization towards an integration of model checking and model updating for system modification.

Original language	English
Title of host publication	Al 2005: Advances in Artificial Intelligence: 18th Australian Joint Conference on Artificial Intelligence, Sydney, Australia, December 5-9, 2005: Proceedings
Publisher	Springer
Number of pages	12
ISBN (Print)	3540304622
Publication status	Published - 2005
Event	Australian Joint Conference on Artificial Intelligence - Duration: 1 Jan 2006 → …

Conference

Conference	Australian Joint Conference on Artificial Intelligence
Period	1/01/06 → …

Keywords

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

Cite this

@inproceedings{6e6e90da3be3428d97a0db6952e5239e,

title = "Model updating CTL systems",

abstract = "Minimal change is a fundamental principle for modelling system dynamics. In this paper, we study the issue of minimal change for Computational Tree Logic (CTL) model update. We first consider five primitive updates which capture the basic update operations in the CTL model. Based on these primitive updates, we then define the minimal change criteria for CTL model update and develop formal algorithms that embed the underlying minimal change principle. We also present the well known microwave oven scenario to demonstrate our update algorithms. Our work presented in this paper can be viewed as the first formalization towards an integration of model checking and model updating for system modification.",

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

author = "Yulin Ding and Yan Zhang and Ray Jarvis and Shichao Zhang",

year = "2005",

language = "English",

isbn = "3540304622",

booktitle = "Al 2005: Advances in Artificial Intelligence: 18th Australian Joint Conference on Artificial Intelligence, Sydney, Australia, December 5-9, 2005: Proceedings",

publisher = "Springer",

note = "Australian Joint Conference on Artificial Intelligence ; Conference date: 01-01-2006",

}

TY - GEN

T1 - Model updating CTL systems

AU - Ding, Yulin

AU - Zhang, Yan

AU - Jarvis, Ray

AU - Zhang, Shichao

PY - 2005

Y1 - 2005

N2 - Minimal change is a fundamental principle for modelling system dynamics. In this paper, we study the issue of minimal change for Computational Tree Logic (CTL) model update. We first consider five primitive updates which capture the basic update operations in the CTL model. Based on these primitive updates, we then define the minimal change criteria for CTL model update and develop formal algorithms that embed the underlying minimal change principle. We also present the well known microwave oven scenario to demonstrate our update algorithms. Our work presented in this paper can be viewed as the first formalization towards an integration of model checking and model updating for system modification.

AB - Minimal change is a fundamental principle for modelling system dynamics. In this paper, we study the issue of minimal change for Computational Tree Logic (CTL) model update. We first consider five primitive updates which capture the basic update operations in the CTL model. Based on these primitive updates, we then define the minimal change criteria for CTL model update and develop formal algorithms that embed the underlying minimal change principle. We also present the well known microwave oven scenario to demonstrate our update algorithms. Our work presented in this paper can be viewed as the first formalization towards an integration of model checking and model updating for system modification.

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/40578

M3 - Conference Paper

SN - 3540304622

BT - Al 2005: Advances in Artificial Intelligence: 18th Australian Joint Conference on Artificial Intelligence, Sydney, Australia, December 5-9, 2005: Proceedings

PB - Springer

T2 - Australian Joint Conference on Artificial Intelligence

Y2 - 1 January 2006

ER -

Model updating CTL systems

Abstract

Conference

Keywords

Other files and links

Fingerprint

Cite this