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