[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.
> Andrew

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.