Abstract:Controller synthesis is the automatic process of searching for a winning strategy in an open real-time system on the basis of a given winning goal. This strategy can be expressed as a series of mapping relations of the symbolic states and the symbolic actions. In this paper, we focus on the reachability target which is described by Linear Temporal Logic(LTL) to discover if there is a synthetic strategy. This paper introduces a synthesis algorithm using on-the-fly method to avoid too many states. The algorithm is an extension of Ref.[1], which is mainly used to solve the problem based on branching temporal logic (CTL) for controller synthesis. Through the use of zone, our algorithm is greatly reducing the number of states, and the efficiency is acceptable.