Comment by steeps | Hacker News Reader

Comment by steeps | Hacker News Reader

One 2EXPTIME-complete problem that I really like is that of Linear Temporal Logic (LTL)[1] realizability. Informally, given a temporal logic formula over inputs and outputs, we can ask whether there exists some program which models the formula over all possible inputs.

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.

[1] https://en.wikipedia.org/wiki/Linear_temporal_logic

Linear Temporal Logic looks very interesting to specify invariant of a system and monitor them at runtime. I guess this is called monitoring. So you can check if your system behaves as expected and e.g. issue an alert if it fails.

There is also Metric Temporal Logic, a special case of Temporal Logic. It allows statement like "There must be an account login (event) 5 minutes before an account deletion." There is also the Signal Temporal Logic, a special case of Temporal Logic. It allows statement like "Whenever the temperatue is over 100 degrees it will be lower than 50 degrees within 10 minutes."

Unfortunately, it seems like it allows to formulate invariants that need an unbounded amount of memory if you monitor infinitely long or a huge amount of memory because the implementation essentially computes a window minimum/maximum function over a large window and has to save all the values in this window.

Do you know if there is a restricted subset of temporal logic that can be monitored fast and with a bounded or even small amount (e.g. O(f(lenght of formula)) of memory?

Could you perhaps recommend some book on computational complexities? My CS curriculum back then mostly included the usual Chomsky hierarchy, but was quite lean on anything other than P/NP, and most books I found were also mostly about the “basics”.

Not the parent but I really enjoyed Scott Aaronson's "Quantum Computing Since Democritus":

https://en.wikipedia.org/wiki/Quantum_Computing_Since_Democr...

Based on:

https://www.scottaaronson.com/democritus/

"Quantum Computing Since Democritus" mentioned in the other answer is definitely good fun, but I find it a bit tricky in places and it very much has a quantum skew. If you're after a textbook reference, then I really like Papadimitriou's Computational Complexity (no longer in print, but used copies/library copies are about) or Arora and Barak's Computational Complexity for something a bit more modern with a nice coverage.

Reply on news.ycombinator.com