ABSTRACT
Formal specifications are used in computer science to specify rigorous requirements for hardware and software systems. This chapter introduces discrete models given by transition systems and formal specifications given by linear temporal logic (LTL) and omega-regular properties. Control synthesis problems are formulated for nondeterministic transition systems, as well as discrete-time and continuous-time dynamical systems, where the latter is formulated under the sample-and-hold control framework. It then discusses how to solve discrete synthesis problems for nondeterministic transition systems with reachability, safety, and general omega-regular specifications. The algorithms are discussed under the formalism of nondeterministic transition systems without converting the controller synthesis problems into a two-player game first. Soundness and completeness of the algorithms are proved, and complexity analysis is provided for each of the algorithms.
