[spoiler]Например, его модели макроскопических систем на основе финслеровых многообразий сегодня активно применяются при построении квантовых систем и в технологиях искусственного фотосинтеза. С 1954 года профессор консультирует американских военных -- на деньги Пентагона в его университете работает институт математических наук, а в 1990 г. Nerode проводил в DARPA семинар по управлению крупными гибридными системами (единый контроль воздушно-наземно-морскими силами) -- тематика, в которой он особо специализируется.
В рамках проекта Domain Specific Software Initiative задумывалось контролировать боевое пространство в реальном времени, но быстро выяснилось, что программная индустрия не готова разрабатывать софт для систем непрерывного управления реального времени, и уж совершенно не было идей, как проверять правильность таких программ. За сутки профессор разработал прототип модели, в которой совмещались дискретная и непрерывная (аналоговая) вычислительные составляющие и реализовывалась концепция взаимодействия таких подсистем в рамках заданных спецификаций. На следующий день состоялась дискуссия, в которой профессор настаивал на необходимости проведения исследовательских работ, однако представитель Boeing напирал на девелоперскую составляющую, ибо назревал контракт на сотни миллионов долларов. В итоге Boeing и занялся этим проектом.
Однако по другим каналам Nerode добился финансирования подобных исследований независимо от DARPA, и в конечном итоге создал теорию гибридных систем, вокруг которой стало формироваться научное коммьюнити. Так, стало понятно, что для формального доказательства корректности гибридной (дискретно-цифровой и непрерывно-аналоговой) системы необходимо совместно применять как механизмы верификации, так и алгоритмы теории управления непрерывными системами.
К подобным технологиям проявляют интерес не только военные, но и промышленность и бизнес. Текущие решения не имеют хорошего математического базиса, и поэтому решают проблемы очень приближенно. Но постепенно ситуация меняется к лучшему -- так, встроенные системы лимузинов Mercedes стали первыми, которые были верифицированы коллегами Nerode из Массачусетса (и возможно, эти автомобили станут первыми настолько умными, что сами удерут с российских дорог обратно в Германию
).Вот мощная работа
http://commonsenseatheism.com/wp-content/uploads/2014/02/Nerode-Logic-and-control.pdf
в которой вкратце рассматривается история вопроса и тематика интеграции PROLOG and Horn Clause Logic, Temporal logics used in Computer Science, Automata logics of BЁuchi, Rabin, Automata theory for finite state transducers of Eilenberg and Schutzenberger, Linear Control, Pontryagin’s optimal control theory, Optimization Theory, Calculus on Banach spaces, Relaxed calculus of variations of L. C. Young and E. J. McShane, Tensor calculus and Cartan exterior differential forms, Differential geometry of geodesics, connections, sprays, Finsler geometry, Variational inequalities, Lie Theory и др.
А вот свободный (GNU) инструментарий KeYmaera
http://symbolaris.com/info/KeYmaera.html
a hybrid verification tool for hybrid systems that combines deductive, real algebraic, and computer algebraic prover technologies. It is an automated and interactive theorem prover for a natural specification and verification logic for hybrid systems.
