  We propose algorithms for performing model checking and control synthesis for
discrete-time uncertain systems under linear temporal logic (LTL)
specifications. We construct temporal logic trees (TLT) from LTL formulae via
reachability analysis. In contrast to automaton-based methods, the construction
of the TLT is abstraction-free for infinite systems, that is, we do not
construct discrete abstractions of the infinite systems. Moreover, for a given
transition system and an LTL formula, we prove that there exist both a
universal TLT and an existential TLT via minimal and maximal reachability
analysis, respectively. We show that the universal TLT is an underapproximation
for the LTL formula and the existential TLT is an overapproximation. We provide
sufficient conditions and necessary conditions to verify whether a transition
system satisfies an LTL formula by using the TLT approximations. As a major
contribution of this work, for a controlled transition system and an LTL
formula, we prove that a controlled TLT can be constructed from the LTL formula
via control-dependent reachability analysis. Based on the controlled TLT, we
design an online control synthesis algorithm, under which a set of feasible
control inputs can be generated at each time step. We also prove that this
algorithm is recursively feasible. We illustrate the proposed methods for both
finite and infinite systems and highlight the generality and online scalability
with two simulated examples.
