  Recently, there has been an increasing interest in the formal analysis and
design of control systems. In this area, in order to reduce the complexity and
scale of control systems, finite abstractions of control systems are introduced
and explored. Amongst, Pola and Tabuada construct finite alternating transition
systems as approximate finite abstractions for control systems with disturbance
inputs [SIAM Journal on Control and Optimization, Vol. 48, 2009, 719-733].
Given linear temporal logical formulas as specifications, this paper provides a
control strategy algorithm to find control strategies of Pola and Tabuada's
abstractions enforcing specifications.
