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

Re: [tlaplus] Verifying fairness | TLC Errors | Refinement | Verifying properties




On 10/21/21 12:09 PM, Travis Allison wrote:
You mentioned, "There are several good textbooks on model checking that explain in detail how that works." Care to give some titles of textbooks you think are good?

Hi Travis,

studying the tableau method shown in "Temporal Verification of Reactive Systems" [1] in addition to "Verifying arbitrary temporal formulas in the temporal logic of actions" [2] would enable you to understand TLC's liveness implementation. More generally, "Principles of Model Checking" [3] is a good introduction.


By the way, Stephan is absolutely right. The fact that TLC does not name the violated properties is due to a highly optimized implementation. I'm happy to give pointers if somebody has the time to address this shortcoming.

Markus

[1] https://www.springer.com/gp/book/9780387944593
[2] http://wischik.com/lu/research/verify-tla-report.pdf
[3] https://mitpress.mit.edu/books/principles-model-checking

--
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/16f4ac23-7f35-004c-920a-a0e997b69fec%40lemmster.de.