Abstract
In the past few years, important applications of nondeterministic finite-transition systems (NFTSs) in formal verification and synthesis of (infinite-state) continuous (or hybrid) control systems have been witnessed (Tabuada 2009; Belta et al. 2017; Kloetzer and Belta 2008; Reissig 2011; Zamani 2014; Girard and Pappas 2007). In this methodology, the requirements or specifications for the control systems are described using temporal logics or automata Baier and Katoen (2008). Then, one constructs finite and often nondeterministic abstractions (NFTSs) of the control systems with the property that discrete (or symbolic) controllers designed on the abstractions by using automata-theoretic algorithms from computer science can be refined into controllers on the original control systems to make the requirements be met.