程序综合是一种通过系统行为规范来自动设计生成交互式系统模型的技术。目前主流的行为规范语言叫做线性时态逻辑LTL。然而LTL程序综合问题是一个复杂的难题,在实践中难以应用。因此基于实践角度考虑,研究者们将更多的关注点放在了LTL子集上的程序综合问题,希望可以有针对性的技术来获得更好的求解方案。本文主要关注一种新的逻辑语言,叫做有限线性时态逻辑LTLf。LTLf对LTL的语法进行了重定义,是一种解析在有限序列上的语言。在这种解析方式下,程序执行序列可以是任意有限长度,也因此令LTLf更加适用于计算机和人工智能领域中的有限域问题。这也就引出了本文的研究课题,LTLf程序综合。本文主要工作和贡献点有以下四个方面:·提出了符号化LTLf程序综合框架。传统的LTLf程序综合方法无法避免空间爆炸问题,于是本文首先提出了符号化DFA的概念,并以此为基础提出了基于BDD和不动点计算的符号化LTLf程序综合框架。实验表明本文提出的新方法在所有已知相关方法中性能最优。·研究了LTLf到DFA的多种编码。从LTLf公式获取DFA是符号化LTLf综合框架中的瓶颈。针对该问题,本文对LTLf的一阶逻辑和二阶逻辑编码进行了比较研究,首次对LTLf二阶逻辑编码进行了探索。首先提出了直观捕获LTLf语法的MSO编码。另外,从自动机最小化理论出发,本文又提出了紧凑MSO编码。该编码利用二阶逻辑公式形式化描述BDD表示的符号化DFA,从而挖掘了BDD和二阶逻辑之间的联系。最后,本文研究发现,在LTLf到DFA的转化问题,一阶逻辑比二阶逻辑更好。·探索了DFA最小化对LTLf综合的影响。DFA构造中的自动机最小化过程具有正反两面性,在产生大量时间消耗的同时却可以帮助综合求解。针对自动机最小化带来的正负影响问题,本文先介绍了一种离线DFA构造方法,首先构造LTLf对应的NFA,然后进行符号化自动机确定化得到DFA,这也避免了自动机最小化过程。比较实验证明,从全局角度看,尽管在离线DFA构造方法上还可以应用动态LTLf综合框架,但是直接采用最小化DFA进行综合计算性能更好。这里的原因主要是,虽然在理论上DFA和NFA相比有着指数级的状态增长,但是实际上最小化DFA可以比NFA更小。这恰恰说明自动机最小化在程序综合中不可或缺。·对LTLf符号化综合框架进行扩展,解决了简单公平假设下的LTLf程序综合问题。该问题相较于LTLf综合而言更加复杂,因为公平假设需要采用LTL公式进行描述。针对该问题,本文基于符号化LTLf综合框架,采用了DFA上的嵌套不动点计算技术,避免了将该问题归约到LTL程序综合的求解方式。实验表明,和所有已知相关方法相比,本文提出的新方法性能最优,这也说明该框架不仅在理论上更加简洁,在实践中也更有潜力。