[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Temporal logic model checking algorithm
On 29.08.19 08:54, 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.
https://www.springer.com/gp/book/9780387944593 and the TLC source code.
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/21f2790c-cc23-ecf4-61b1-919e006bff6a%40lemmster.de.