Weighted O-Minimal Hybrid Systems Are More Decidable Than Weighted Timed Automata!
Weighted O-Minimal Hybrid Systems Are More Decidable Than Weighted Timed Automata!
复制标题
加权 O-最小混合系统比加权定时自动机更具可判定性！
DOI：
--
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
Fabrice Chevalier
中科院分区：
文献类型：
--
作者：
P. Bouyer;Thomas Brihaye;Fabrice Chevalier
我们考虑加权o-极小混杂系统，它用代价函数推广了经典的o-极小混杂系统。这些成本函数是“观察者变量”，随着系统的发展而增加，但不会约束系统的行为。在本文中，我们证明了两个主要结果：(I)最优o-极小混合对策是可判定的；(Ii)WCTL的模型检验是可判定的，WCTL是CTL的扩展，它可以约束代价变量。这必须与时间自动机框架中的相同问题进行比较，在时间自动机框架中，这两个问题通常都是不可判定的，而对于受限类别的单时钟时间自动机来说，它们是可判定的。
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.