Efficient controller synthesis for a fragment of MTL<inf>0</inf>, &infin

ISCAS OpenIR

	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
发表期刊	Acta Informatica
ISSN	15903
卷号	51 期号:3-4 页码:165-192
摘要	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
部门归属	(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
语种	英语
内容类型	期刊论文
URI标识	http://ir.iscas.ac.cn/handle/311060/16861
专题	中国科学院软件研究所
通讯作者	Bulychev, P.(peter.bulychev@gmail.com)
推荐引用方式 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.