[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Re: Temporal logic model checking algorithm

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.


You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/ea9b0f4e-e509-4ed0-809c-c473d78555cf%40googlegroups.com.