Name
Abstract | ||
|---|---|---|
To deal with the model checking issue of rectangular hybrid systems, a constraint system called hybrid zone is introduced for the representation and manipulation of rectangular hybrid automata state-spaces. Model checking procedures for rectangular hybrid systems based on timed computation tree logic are given. The hybrid zone is proved to be closed to the operations required in these model checking procedures, which enables it to be used as the basis for the infinite state-space exploring of rectangular hybrid automata. To represent hybrid zones, a data structure difference constraint matrix is introduced. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1109/TASE.2010.18 | TASE |
Keywords | Field | DocType |
automata theory,hybrid systems,rectangular hybrid automata state-spaces,model checking issue,rectangular hybrid automata state-space manipulation,difference constraint matrix,model checking,rectangular hybrid system,timed computation tree logic,infinite state-space,constraint system,model checking procedure,model checking rectangular hybrid,rectangular automata,timed computing tree logic,temporal logic,model checking rectangular hybrid system,rectangular hybrid automaton,computation tree logic,formal verification,data structure difference constraint,hybrid zone,state space,automata,computational modeling,cost accounting,data structure,state space model,hybrid system,labeling | Computation tree logic,Data structure,Automata theory,Model checking,Computer science,Automaton,Algorithm,Theoretical computer science,Temporal logic,Hybrid system,Formal verification | Conference |
ISBN | Citations | PageRank |
978-1-4244-7847-7 | 1 | 0.38 |
References | Authors | |
10 | 5 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Haibin Zhang | 1 | 118 | 18.58 |
| Zhenhua Duan | 2 | 658 | 78.37 |
| Bohu Huang | 3 | 2 | 1.40 |
| Xiaobing Wang | 4 | 33 | 7.86 |
| Long Zhang | 5 | 13 | 7.45 |