A logical approach to qualitative analysis of controlled nonlinear binary dynamic systems

Abstract

The problems of a qualitative study of the trajectories behavior dynamics of controlled nonlinear binary dynamic systems on a finite time interval are considered using the method of Boolean constraints. Models of local dynamic properties, the trajectories periodicity property, and controllability type properties are obtained in the form of Boolean constraints. Depending on the property, the verification of Boolean constraints is reduced to the Boolean satisfiability problem or the problem of verifying the truth of a quantified Boolean formula.