Name
Abstract | ||
|---|---|---|
We consider weighted o-minimal hybrid systems, which extend classical o-minimal hybrid systems with cost functions. These cost functions are "observer variables" which increase while the system evolves but do not constrain the behaviour of the system. In this paper, we prove two main results: (i) optimal o-minimal hybrid games are decidable; (ii) the model-checking of WCTL, an extension of CTL which can constrain the cost variables, is decidable over that model. This has to be compared with the same problems in the framework of timed automata where both problems are undecidable in general, while they are decidable for the restricted class of one-clock timed automata. |
Year | DOI | Venue |
|---|---|---|
2007 | 10.1007/978-3-540-72734-7_6 | LFCS |
Keywords | Field | DocType |
main result,optimal o-minimal hybrid game,classical o-minimal hybrid system,system evolves,weighted timed automata,weighted o-minimal hybrid systems,o-minimal hybrid system,cost variable,cost function,observer variable,restricted class,hybrid system,model checking | Discrete mathematics,Computer science,Automaton,Decidability,Timed automaton,Optimal cost,Observer (quantum physics),Hybrid system,Hybrid automaton,Undecidable problem | Conference |
Volume | ISSN | Citations |
4514 | 0302-9743 | 8 |
PageRank | References | Authors |
0.55 | 23 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Patricia Bouyer | 1 | 735 | 37.19 |
| Thomas Brihaye | 2 | 460 | 35.91 |
| Fabrice Chevalier | 3 | 126 | 7.32 |