Template-Based Controller Synthesis for Timed Systems
Template-Based Controller Synthesis for Timed Systems
复制标题
定时系统基于模板的控制器综合
DOI：
10.1007/978-3-642-28756-5_27
复制
发表时间：
2012
影响因子：
5.2
通讯作者：
H. Peter
中科院分区：
文献类型：
--
作者：
B. Finkbeiner;H. Peter
我们为实时系统提供了一种有效的控制器合成方法，该实时系统以安全要求为定时自动机。在局部可观察性的现实假设下，如果提前对控制器的粒度结合，则该问题通常是不确定的，并且非常昂贵（2Exptime-Complete）。我们研究了具有参数控制结构的定时自动机的控制器的合成。基于模板的合成比标准合成显着（PSPACE-COMPLETE）明显便宜，并且会产生更简单的控制器。我们提出了一种基于自动抽象细化的有效符号合成算法，并报告了在定时验证和合成工具合成中实现的实验结果的报告。
We present an effective controller synthesis method for real-time systems modeled as timed automata with safety requirements. Under the realistic assumption of partial observability, the problem is undecidable in general, and prohibitively expensive (2ExpTime-complete) if a bound on the granularity of the controller is set in advance. We investigate the synthesis of controllers from templates, given as timed automata with parametric control structure. Template-based synthesis is significantly cheaper (PSpace-complete) than standard synthesis and produces much simpler controllers. We present an efficient symbolic synthesis algorithm based on automatic abstraction refinement and report on encouraging experimental results from an implementation in the timed verification and synthesis tool synthia.