@inproceedings{BakBogomolovHenceyetal.2022, author = {Bak, Stanley and Bogomolov, Sergiy and Hencey, Brandon and Kochdumper, Niklas and Lew, Ethan and Potomkin, Kostiantyn}, title = {Reachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope Refinement}, booktitle = {Computer Aided Verification: 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part I}, editor = {Shoham, Sharon and Vizel, Yakir}, publisher = {Springer}, address = {Cham}, isbn = {978-3-031-13185-1}, doi = {https://doi.org/10.1007/978-3-031-13185-1_24}, pages = {490 -- 510}, year = {2022}, abstract = {Koopman operator linearization approximates nonlinear systems of differential equations with higher-dimensional linear systems. For formal verification using reachability analysis, this is an attractive conversion, as highly scalable methods exist to compute reachable sets for linear systems. However, two main challenges are present with this approach, both of which are addressed in this work. First, the approximation must be sufficiently accurate for the result to be meaningful, which is controlled by the choice ofobservable functionsduring Koopman operator linearization. By using random Fourier features as observable functions, the process becomes more systematic than earlier work, while providing a higher-accuracy approximation. Second, although the higher-dimensional system is linear, simple convex initial sets in the original space can become complex non-convex initial sets in the linear system. We overcome this using a combination of Taylor model arithmetic and polynomial zonotope refinement. Compared with prior work, the result is more efficient, more systematic and more accurate.}, language = {en} } @inproceedings{LewHekalPotomkinetal.2023, author = {Lew, Ethan and Hekal, Abdelrahman and Potomkin, Kostiantyn and Kochdumper, Niklas and Hencey, Brandon and Bak, Stanley and Bogomolov, Sergiy}, title = {AutoKoopman: A Toolbox for Automated System Identification via Koopman Operator Linearization}, booktitle = {Automated Technology for Verification and Analysis: 21st International Symposium, ATVA 2023, Singapore, October 24-27, 2023, Proceedings, Part II}, editor = {Andr{\´e}, {\´E}tienne and Sun, Jun}, publisher = {Springer}, address = {Cham}, isbn = {978-3-031-45332-8}, doi = {https://doi.org/10.1007/978-3-031-45332-8_12}, pages = {237 -- 250}, year = {2023}, language = {en} } @article{BakBogomolovHenceyetal.2025, author = {Bak, Stanley and Bogomolov, Sergiy and Hencey, Brandon and Kochdumper, Niklas and Lew, Ethan and Potomkin, Kostiantyn}, title = {Reachability of Koopman linearized systems using explicit kernel approximation and polynomial zonotope refinement}, volume = {66}, journal = {Formal Methods in System Design}, number = {2}, publisher = {Springer}, address = {Dordrecht}, issn = {1572-8102}, doi = {https://doi.org/10.1007/s10703-024-00464-z}, pages = {307 -- 333}, year = {2025}, language = {en} }