Is anyone familiar with temporal logics and have seen/done any FoC projects using them?

Temporal logic means different things to different people. I suggest you refine your question so that the answers are more relevant to your purposes. My Beads language runtime has an automatic temporal logic built in, that schedules affected portions of the screen for refresh based on changes in the underlying model. It is an invisible system that saves the programmer the trouble of calculating for every microscopic change in the underlying model, which layout/drawing functions need to be called again. This is very useful for a 2D world, but to be frank many people are using 3D interfaces now and they refresh the whole model on every single frame, so they don't have to bother guessing which part to redraw (under-draw causes glitches, and over-draw slows the product down). There is a certain brute-force simplicity to stored 3D graphics. It also can run backwards post-mortem, which is a temporal operation that is extremely useful for debugging client problems. One of the biggest problems facing software today is the inability for companies to replicate intermittent problems, based on complex user-specific data values, with the result that companies like MS, Apple and Adobe have hundreds of thousands if not millions of open bugs reported that the vast majority of fall into the category "cannot duplicate" so they fester in their bug reporting systems. We are in an era where consumers accept sloppy products that are riddled with minor bugs, and i find it personally abhorrent that it is so acceptable. With so many projects grown to a size where a single person cannot understand the product from top to bottom, we are in a very dark age IMHO.

I mean "temporal logic"(s) in the sense of "propositional logic" or "predicate logic". It's a niche mathematical topic, and I don't expect many people to know anything about it. I thought it was worth asking though!

Actually the deduction of what sections of the screen drawing functions need to be executed again is predicate logic, where logical implication is being calculated automatically. This saves you the trouble of writing all the implication rules for every microscopic change in your model. As the number of controls grows on the screen, the number of interactions between the widgets on the screen can grow exponentially. This is a feature directly borrowed from PROLOG and it is not common. The Unix Make build tool language uses an explicit predicate logic for example, and another example of automatic predicate logic in Beads is the compiler's module system which is borrowed from Modula-2 whereby you can specify imports very simply and it builds the total list of modules to compile, and does them in the correct order. The key thing with predicate logic is to try and avoid having users write the predicates explicitly, because they are not easy to construct. The average programmer knows simple boolean logic but long predicate chains are downright opaque to most. One should always keep in mind the example of Principia Mathematica by Russell & Whitehead, which took something on the order of 100 pages of gibberish to prove 1+1 = 2. Logical purity is an altar on which you can sacrifice all productivity.