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 | AI 2005 |
| Subtitle of host publication | Advances in Artificial Intelligence - 18th Australian Joint Conference on Artificial Intelligence, Proceedings |
| Pages | 5-16 |
| Number of pages | 12 |
| DOIs | |
| Publication status | Published - 2005 |
| Event | 18th Australian Joint Conference on Artificial Intelligence, AI 2005: Advances in Artificial Intelligence - Sydney, Australia Duration: 5 Dec 2005 → 9 Dec 2005 |
Publication series
| Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
|---|---|
| Volume | 3809 LNAI |
| ISSN (Print) | 0302-9743 |
| ISSN (Electronic) | 1611-3349 |
Conference
| Conference | 18th Australian Joint Conference on Artificial Intelligence, AI 2005: Advances in Artificial Intelligence |
|---|---|
| Country/Territory | Australia |
| City | Sydney |
| Period | 5/12/05 → 9/12/05 |