66 karma · joined November 17, 2021
For instance, if we label the undesirable outputs as BAD, then we can write a formula like G!BAD (read: always not BAD), and ask if there exists a program which models this formula - if there does, then we know there's some program which never enters the undesirable states, regardless of the input. You can extend this from a decision problem (yes/no answers) to synthesis, and construct such a program using similar techniques (I'm using "program" in a very specific sense here - much of the current art is focused around finite-state automata).
Shameless plug: I wrote my thesis on decision problems around the existence of game-theoretic solutions concepts (e.g. Nash equilibria, the Core) in multi-agent systems and many of these were 2EXPTIME-complete. A lot of the time you could easily show membership in 2EXPTIME by making an exponential(!) number of relevant calls to the LTL realizability problem.
If instead, you want to focus on neural networks, I found Michael Nielsen's Neural Networks and Deep Learning an excellent resource for implementing them from first principles (available at http://neuralnetworksanddeeplearning.com/).
[1]: https://nitter.net/kenjilopezalt/status/1176542696724320256