Temporal logic model checking algorithm

[Andrew Helwer]

Are there any good resources on the algorithm TLC uses to model-check temporal properties? Safety invariants are easy enough (just BFS/DFS through all states) but temporal properties seem like they have a ton of edge cases.

I'm looking for something with enough detail that I could implement the algorithm in my own toy model-checker.

Andrew

[Markus Kuppe]

https://www.springer.com/gp/book/9780387944593 and the TLC source code.

M.

[Andrew Helwer]

To anyone else who has found this thread and is curious, the current reference is "The Handbook of Model Checking" (less of a handbook and more of an enormous tome, really) which is found here: https://www.springer.com/gp/book/9783319105741