|
| 作者 | Bulychev, Peter (1)
; David, Alexandre (1)
; Larsen, Kim G. (1)
; Li, Guangyuan (2)
|
| 刊名 | Acta Informatica
 |
| 出版日期 | 2014
|
| 卷号 | 51期号:3-4页码:165-192 |
| ISSN号 | 15903
|
| 通讯作者 | Bulychev, P.(peter.bulychev@gmail.com)
|
| 中文摘要 | In this paper we offer an efficient controller synthesis algorithm for assume-guarantee specifications of the form φ1 ∧ φ2 ∧ &mellip; ∧ φn → ψ1 ∧ ψ2 ∧ &mellip; ∧ ψm. Here, {φi,ψj} are all safety-MTL0, ∞ properties, where the sub-formulas {φi} are supposed to specify assumptions of the environment and the sub-formulas {ψj} are specifying requirements to be guaranteed by the controller. Our synthesis method exploits the engine of Uppaal-Tiga and the novel translation of safety- and co-safety-MTL0, ∞ properties into under-approximating, deterministic timed automata. Our approach avoids determinization of Bu¨chi automata, which is the main obstacle for the practical applicability of controller synthesis for linear-time specifications. The experiments demonstrate that the chosen specification formalism is expressive enough to specify complex behaviors. The proposed approach is sound but not complete. However, it successfully produced solutions for all the experiments. Additionally we compared our tool with Acacia+ and Unbeast, state-of-the-art LTL synthesis tools; and our tool demonstrated better timing results, when we applied both tools to the analogous specifications. © 2013 Springer-Verlag Berlin Heidelberg. |
| 英文摘要 | In this paper we offer an efficient controller synthesis algorithm for assume-guarantee specifications of the form φ1 ∧ φ2 ∧ &mellip; ∧ φn → ψ1 ∧ ψ2 ∧ &mellip; ∧ ψm. Here, {φi,ψj} are all safety-MTL0, ∞ properties, where the sub-formulas {φi} are supposed to specify assumptions of the environment and the sub-formulas {ψj} are specifying requirements to be guaranteed by the controller. Our synthesis method exploits the engine of Uppaal-Tiga and the novel translation of safety- and co-safety-MTL0, ∞ properties into under-approximating, deterministic timed automata. Our approach avoids determinization of Bu¨chi automata, which is the main obstacle for the practical applicability of controller synthesis for linear-time specifications. The experiments demonstrate that the chosen specification formalism is expressive enough to specify complex behaviors. The proposed approach is sound but not complete. However, it successfully produced solutions for all the experiments. Additionally we compared our tool with Acacia+ and Unbeast, state-of-the-art LTL synthesis tools; and our tool demonstrated better timing results, when we applied both tools to the analogous specifications. © 2013 Springer-Verlag Berlin Heidelberg. |
| 收录类别 | SCI
; EI
|
| 语种 | 英语
|
| 公开日期 | 2014-12-16
|
| 源URL | [http://ir.iscas.ac.cn/handle/311060/16861]  |
| 专题 | 软件研究所_软件所图书馆_期刊论文
|
推荐引用方式
GB/T 7714 |
Bulychev, Peter ,David, Alexandre ,Larsen, Kim G. ,et al. Efficient controller synthesis for a fragment of MTL0, &infin[J]. Acta Informatica,2014,51(3-4):165-192.
|
| APA |
Bulychev, Peter ,David, Alexandre ,Larsen, Kim G. ,&Li, Guangyuan .(2014).Efficient controller synthesis for a fragment of MTL0, &infin.Acta Informatica,51(3-4),165-192.
|
| MLA |
Bulychev, Peter ,et al."Efficient controller synthesis for a fragment of MTL0, &infin".Acta Informatica 51.3-4(2014):165-192.
|
