Loading...
Please wait, while we are loading the content...
Similar Documents
Handling Inconsistencies in CTL Model-Checking using Belief Revision
| Content Provider | Semantic Scholar |
|---|---|
| Author | Sousa, Thiago Wassermann, Renata |
| Copyright Year | 2007 |
| Abstract | Given a formal description of a system, there are computatio n l tools that verify the validity of some properties in the system. Th ese tools usually only tell the user whether the property holds or not, without givi ng any hint as to how the system could be adapted in order for the desired property to hold. In this paper, we present a formal approach for handling inco sistencies in CTL (computation tree logic) model-checking using belief revi sion. Given a CTL formula inconsistent with a model of the system described in SMV, we revise this model in such a way that the formula becomes true. This revisi on forces changes in the SMV description of the system. Our implementation enr iches the NuSMV model checker with three types of change: addition of lines, elimination of lines and change in the initial state, where the first two cause modi ficat ons in the transitions between the states of the model. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://www.ime.usp.br/~renata/papers/artigo-sbmf4.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
