Idea of Symbolic Computation of Reachable States

This lecture introduces the concept of symbolic computation of reachable states in transition systems. It covers the definition of transition systems, the properties of the function G, the sequence of states in a transition system, and a reachability procedure using fixed points. The lecture also explains how to implement the reachability procedure, a symbolic algorithm, and the use of non-normalized formulas in symbolic computation. The instructor discusses the termination of algorithms for finite-state systems and the importance of simplifying and normalizing formulas to avoid exponential blowup.