Counterexample-Guided Synthesis of Observation Predicates
Counterexample-Guided Synthesis of Observation Predicates
复制标题
反例引导的观察谓词合成
DOI：
10.1007/978-3-642-33365-1_9
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
B. Finkbeiner
中科院分区：
文献类型：
--
作者：
R. Dimitrova;B. Finkbeiner
我们提出了一种新颖的方法来解决安全控制器综合问题，并具有实时系统的部分可观测性。通过固定控制器的粒度，可以将这一通常不可判定的问题简化为可判定的问题：守卫中的有限时钟集和常量。当前最先进的方法仅限于对可能的粒度进行强力枚举或手动选择控制器可以跟踪的有限观察集。我们通过提出一种反例引导的方法来解决这一限制，该方法可以连续细化一组观察结果，直到获得足够精确的抽象。我们的方法生成的抽象博弈和策略的大小取决于观察谓词的数量，而不是植物中常数的大小。我们的实验表明，当需要细粒度时，这比基于固定粒度的方法具有更好的性能。
We present a novel approach to the safety controller synthesis problem with partial observability for real-time systems. This in general undecidable problem can be reduced to a decidable one by fixing the granularity of the controller: finite sets of clocks and constants in the guards. Current state-of-the-art methods are limited to brute-force enumeration of possible granularities or manual choice of a finite set of observations that a controller can track. We address this limitation by proposing a counterexample-guided method to successively refine a set of observations until a sufficiently precise abstraction is obtained. The size of the abstract games and strategies generated by our approach depends on the number of observation predicates and not on the size of the constants in the plant. Our experiments demonstrate that this results in better performance than the approach based on fixed granularity when fine granularity is necessary.
登录
查看更多内容
影响因子：
5.2
作者：
Rayna Dimitrova;B. Finkbeiner
通讯作者：
B. Finkbeiner
影响因子：
5.2
作者：
F. Cassez;Alexandre David;K. Larsen;D. Lime;Jean
通讯作者：
Jean
DOI：
10.1016/j.ic.2009.05.007
发表时间：
2007
期刊：
52nd IEEE Conference on Decision and Control
影响因子：
--
作者：
L. D. Alfaro;Pritam Roy
通讯作者：
Pritam Roy
具有部分可观测性的定时控制
影响因子：
5.2
作者：
P. Bouyer;D. D'Souza;Madhusudan Parthasarathy;A. Petit
通讯作者：
A. Petit
定时系统基于模板的控制器综合
影响因子：
5.2
作者：
B. Finkbeiner;H. Peter
通讯作者：
H. Peter