Functionally-Equivalent Formalization and Automated Model Checking of Function Block Diagrams. - Tomás Ausberger; Karel Kubícek 002; Pavla Medvedcova (IEEE Access, 2025)