  The search for Lyapunov functions is a crucial task in the analysis of
nonlinear systems. In this paper, we present a physics-informed neural network
(PINN) approach to learning a Lyapunov function that is nearly maximal for a
given stable set. A Lyapunov function is considered nearly maximal if its
sub-level sets can be made arbitrarily close to the boundary of the domain of
attraction. We use Zubov's equation to train a maximal Lyapunov function
defined on the domain of attraction. Additionally, we propose conditions that
can be readily verified by satisfiability modulo theories (SMT) solvers for
both local and global stability. We provide theoretical guarantees on the
existence of maximal Lyapunov functions and demonstrate the effectiveness of
our computational approach through numerical examples.
