Loading...
Please wait, while we are loading the content...
Similar Documents
Fast equational abstraction refinement for regular tree model checking (2010).
| Content Provider | CiteSeerX |
|---|---|
| Author | Boichut, Y. Boyer, B. Genet, T. Legay, A. |
| Abstract | ABSTRACT. Tree Regular model checking is the name of a family of techniques for analyzing infinitestate systems in which states are represented by trees and sets of states by tree automata. From the verification point of view, the central problem is to compute the set of reachable states providing a given transition relation. A main obstacle is that this set is in general not computable in a finite time. In this paper, we propose a new CounterExample Guided Abstraction Refinement technique that can be used to check whether a set of state can be reached from the initial set. Contrary to existing techniques, our approach relies on equational abstraction to ease the definition of approximations and on a specific model of tree automata to avoid heavy backward refinement steps. 1 |
| File Format | |
| Publisher Date | 2010-01-01 |
| Access Restriction | Open |
| Subject Keyword | Fast Equational Abstraction Refinement Regular Tree Model Checking Tree Automaton Central Problem Approach Relies Finite Time Specific Model Transition Relation Verification Point Main Obstacle Heavy Backward Refinement Step Initial Set Tree Regular Model Checking Reachable State Infinitestate System Equational Abstraction |
| Content Type | Text |
| Resource Type | Article |
