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
On Thursday, August 29, 2019 at 8:54:02 AM UTC-7, Andrew Helwer wrote:
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