Formal verification of stability and chaos in periodic optical systems

Optical systems are widely used in a wide range of safety, cost and mission-critical applications including biomedical devices and high-speed communication networks. Therefore, modeling and verification of such high-consequence systems is crucial for both theoretical and application viewpoints. In this paper, we propose a formal methods based approach to model and verify the properties of periodic optical systems which allow a cyclic passage of light through a sequence of optical components. We focus on two important properties namely stability and chaotic map generation which ensure the confinement of light and chaos generation, respectively. We use higher-order logic as a specification and reasoning framework and develop a library of necessary notions of periodic optical systems. Consequently, we demonstrate the utilization and effectiveness of our development by a couple of case studies: a Fabry Pérot resonator with fiber-rod lens and a phase-conjugated ring resonator.