We suggest an expressive fragment of LTL for which reactive synthesis can be performed by symbolically analyzing games. For general LTL, this kind of analysis is impossible due to the complexity of determinization. Bypasses are either by enumerative handling of determinization or by restricting attention to fragments of the language. Here, we take the second approach and suggest a fragment combining a safety specification and a liveness part. The safety part is unrestricted but allows symbolic treatment due to the simplicity of determinization in the case of safety languages. The liveness part is very general, allowing to define Emerson-Lei conditions on occurrences of letters. We elaborate the construction of an Emerson-Lei game that captures the synthesis problem. We also show how Emerson-Lei games can be analyzed symbolically by providing a fixpoint-based characterization of the winning region, which is obtained from an analysis of the Zielonka tree of the winning condition. Our algorithm generalizes the solutions of games with known winning conditions such as B\"uchi, GR[1], parity, Streett, Rabin and Muller objectives, and in the case of these conditions reproduces previously known algorithms and complexity results; the algorithm solves unrestricted Emerson-Lei games with $n$ nodes, $m$ edges and $k$ colors in time $\mathcal{O}(k!\cdot m\cdot n^k)$ and yields winning strategies with memory $\mathcal{O}(k!)$. The runtime of the resulting overall synthesis algorithm is single-exponential in the size of the liveness part and doubly-exponential in the size of the safety part, as it is for (safety) LTL. However, the trade-off between enumerative and symbolic aspects is maximized by enumeratively analyzing the liveness condition and generating from it a symbolic game analysis algorithm.


翻译:暂无翻译

0
下载
关闭预览

相关内容

Stabilizing Transformers for Reinforcement Learning
专知会员服务
54+阅读 · 2019年10月17日
《DeepGCNs: Making GCNs Go as Deep as CNNs》
专知会员服务
30+阅读 · 2019年10月17日
强化学习最新教程,17页pdf
专知会员服务
166+阅读 · 2019年10月11日
机器学习入门的经验与建议
专知会员服务
89+阅读 · 2019年10月10日
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
96+阅读 · 2019年10月9日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
39+阅读 · 2019年10月9日
Hierarchically Structured Meta-learning
CreateAMind
23+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
24+阅读 · 2019年5月18日
19篇ICML2019论文摘录选读!
专知
28+阅读 · 2019年4月28日
逆强化学习-学习人先验的动机
CreateAMind
15+阅读 · 2019年1月18日
Unsupervised Learning via Meta-Learning
CreateAMind
41+阅读 · 2019年1月3日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
15+阅读 · 2018年12月24日
disentangled-representation-papers
CreateAMind
26+阅读 · 2018年9月12日
vae 相关论文 表示学习 1
CreateAMind
12+阅读 · 2018年9月6日
【推荐】RNN/LSTM时序预测
机器学习研究会
25+阅读 · 2017年9月8日
国家自然科学基金
3+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2008年12月31日
Arxiv
0+阅读 · 2023年6月15日
Arxiv
11+阅读 · 2021年12月8日
VIP会员
相关VIP内容
Stabilizing Transformers for Reinforcement Learning
专知会员服务
54+阅读 · 2019年10月17日
《DeepGCNs: Making GCNs Go as Deep as CNNs》
专知会员服务
30+阅读 · 2019年10月17日
强化学习最新教程,17页pdf
专知会员服务
166+阅读 · 2019年10月11日
机器学习入门的经验与建议
专知会员服务
89+阅读 · 2019年10月10日
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
96+阅读 · 2019年10月9日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
39+阅读 · 2019年10月9日
相关资讯
Hierarchically Structured Meta-learning
CreateAMind
23+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
24+阅读 · 2019年5月18日
19篇ICML2019论文摘录选读!
专知
28+阅读 · 2019年4月28日
逆强化学习-学习人先验的动机
CreateAMind
15+阅读 · 2019年1月18日
Unsupervised Learning via Meta-Learning
CreateAMind
41+阅读 · 2019年1月3日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
15+阅读 · 2018年12月24日
disentangled-representation-papers
CreateAMind
26+阅读 · 2018年9月12日
vae 相关论文 表示学习 1
CreateAMind
12+阅读 · 2018年9月6日
【推荐】RNN/LSTM时序预测
机器学习研究会
25+阅读 · 2017年9月8日
相关基金
国家自然科学基金
3+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2008年12月31日
Top
微信扫码咨询专知VIP会员