Weighted o-minimal hybrid systems |
| |
Authors: | Patricia Bouyer Thomas Brihaye Fabrice Chevalier |
| |
Institution: | aLSV - CNRS & ENS de Cachan, 61, Avenue du Président Wilson, 94230 Cachan, France;bUniversité de Mons, 20, Place du Parc, 7000 Mons, Belgium |
| |
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. |
| |
Keywords: | O-minimal hybrid systems Games Model checking Temporal logic Decidability |
本文献已被 ScienceDirect 等数据库收录! |
|