| Efficient controller synthesis for a fragment of MTL0, &infin |
| Bulychev, Peter (1); David, Alexandre (1); Larsen, Kim G. (1); Li, Guangyuan (2); Bulychev, P.(peter.bulychev@gmail.com)
|
| 2014
|
| Source | Acta Informatica
 |
| ISSN | 15903
|
| Volume | 51Issue:3-4Pages:165-192 |
| English Abstract | 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. |
| Indexed Type | SCI
; EI
|
| Department | (1) CISS, CS, Aalborg University, Ålborg, Denmark; (2) State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China; (3) Google Inc., Zurich, Switzerland, CA, United States
|
| Language | 英语
|
| Content Type | 期刊论文
|
| URI | http://ir.iscas.ac.cn/handle/311060/16861
|
| Collection | 中国科学院软件研究所
|
| Corresponding Author | Bulychev, P.(peter.bulychev@gmail.com) |
Recommended Citation
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 ,&Bulychev, P..(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.
|
| Files in This Item: |
|
There are no files associated with this item. |
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment