中文摘要：

利用有限抽象进行控制系统的形式化分析与设计是目前研究较多的一类控制系统分析与设计方法．本文提出两种方法，使用有限抽象，构造出两种控制器，使带扰动的控制系统满足时序逻辑规范．为此，首先在时序逻辑规范上引入“弱化”转换函数和“强化”转换函数．进而，利用“弱化”转换函数提出一种方法用于构造控制器，使原系统近似满足给定规范；利用“强化”转换函数，提出另一种方法用于构造控制器，使原系统严格满足给定规范．本文分析比较上述两种方法与文献中已有的方法，指出各自的优缺点和适用范围．最后给出仿真实验，说明上述两种方法的有效性并展示这些方法的不同适用范围．

英文摘要：

Adopting finite abstraction for the formal analysis and design of control systems is prevailing recently. By applying finite abstractions, we develop two methods for constructing the controller for systems with disturbances so that these systems will satisfy temporal logical specifications. To this end, we first introduce the ＂weaken＂ transformation function and the ＂strengthen＂ transformation function for the temporal logical specifications. By using the ＂weaken＂ transformation function, we develop a method to construct the controller forcing the controlled systems with disturbances to approximately satisfy the specifications. Then, we use the ＂strengthen＂ transformation function to develop another method to construct the other controller enforcing the controlled system to exactly satisfy the specifications. We compare these two methods with some existing methods in modem literature, and find out the advantages and application scopes of these methods. Finally, a simulation example is presented to demonstrate the validity and different application scopes of these two methods.