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

Re: [tlaplus] Why TLA+ is based on explicit state model-checking instead of symbolic one?

Hello Evgeniy,

symbolic model checking is not easy to implement for an expressive language such as TLA+. For example, some form of type inference is necessary in order to know how to symbolically represent the value of a variable. The explicit construction of successor states by interpreting the next-state relation is much easier to implement. Moreover, it is not a given that symbolic model checking is always superior to explicit-state model checking. For example, asynchronous systems whose processes communicate via FIFO channels tend to give rise to state spaces for which no good symbolic representation is known.

However, a symbolic model checker for TLA+ is being built [1], and we hope that it will become a useful complement to TLC. You may also want to experiment with ProB that supports a subset of TLA+ [2] and contains implementations of symbolic model checking algorithms [3].

Best regards,

[1] http://forsyte.at/research/apalache/
[2] https://www3.hhu.de/stups/prob/index.php/ProB_for_TLA 
[3] https://www3.hhu.de/stups/prob/index.php/Symbolic_Model_Checking

On 4 Jul 2018, at 10:24, Evgeniy Shishkin <evgeniy....@xxxxxxxxx> wrote:

Hello researchers!

Relying on the fact that this forum is inhabited with inventors of TLA+, I would really like
to know the answer.


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+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.