Name
Abstract | ||
|---|---|---|
Model update is an approach to enhance model checking functions by providing computer aided modifications in system development [2, 9]. It has been observed that one major obstacle restricting the application of this approach, e.g. CTL model update [15], is that the update has to take the entire system model into account, and that is usually not feasible for large scale domains. In this paper, we develop a tree-like local model update approach under the framework of ACTL --a widely used fragment of CTL in property specification. We define a bisimulation based minimal change principle on tree-like local model update, reveal its relationship to traditional belief update and provide essential semantic characterizations. We also investigate primary semantic and computational properties in relation to tree-like local model update. Finally we briefly describe the update system prototype that we have implemented and summarize our experimental results. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.3233/978-1-60750-606-5-615 | ECAI |
Keywords | Field | DocType |
update system prototype,local model update,tree-like local model updates,system development,essential semantic characterization,tree-like local model update,model update,ctl model update,entire system model,traditional belief update,model checking function | Obstacle,Model checking,Computer-aided,Computer science,Artificial intelligence,Bisimulation,System development,System model | Conference |
Volume | ISSN | Citations |
215 | 0922-6389 | 2 |
PageRank | References | Authors |
0.40 | 11 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Yan Zhang | 1 | 777 | 123.70 |
| Michael Kelly | 2 | 7 | 1.20 |
| Yi Zhou | 3 | 161 | 26.62 |