Why TLA+ is based on explicit state model-checking instead of symbolic one?

[Evgeniy Shishkin]

Hello researchers!

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

to know the answer.

Thanks.

[Stephan Merz]

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,

Stephan

[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

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

[Igor Konnov]

Hi Evgeniy,

Stephan already mentioned some issues. I would like to comment on our experience when developing such a symbolic model checker for TLA+ [1]. The web page is more up-to-date now.

1. There are no built-in types in TLA+. On one hand, TLC nicely avoids this issue, as it computes values dynamically and reports a type mismatch exactly when it happens. In this sense it acts as an interpreter, not a compiler. On the other hand, symbolic techniques work more like a compiler, that is, they translate a specification into a symbolic transition system: binary decision diagrams (BDDs), Boolean formulas (SAT), first-order theories (SMT), constraints over integer variables, etc. To do such a translation one needs to statically find proper types.

2. One has to find a good encoding of TLA+ expressions in the target symbolic representation. When using BDDs or SAT solvers, one has to translate all kinds of TLA+ expressions into Boolean formulas. While it is not conceptually hard for fix-width integers or tuples, it becomes tricky for sets and functions. A naive translation of the expression "x \in SUBSET {1, 2, 3}" would just compute all the subsets before constructing symbolic constraints, which defeats the purpose of using symbolic techniques.

It is somewhat easier with the SMT solvers that support integers, arrays, uninterpreted functions, etc. However, one still has to find good ways to translate sets, sets of sets, sets of functions, set cardinalities, etc.

We believe that we have come up with a good SMT encoding for a large part of TLA+ expressions that can be found in the actual TLA+ code. But the tool is still far from being useful. When it is ready for any kind of testing, we will announce it on the list. 

Best regards,

Igor

[1] http://forsyte.at/research/apalache/

[Ron Pressler]

I believe Stephan has a number of papers describing his (and others') work on inferring types for TLA+ expressions for use in TLAPS, but your description of interpreters vs. compilers (while there is no real formal difference due to partial evaluation theorems, there is a clear practical difference) made me think of an idea that I wonder if anyone has explored. 

Both compilers and modern model checkers are based on sound abstractions, which, at its most primitive level, correspond to the simple types that compilers can employ so well to emit efficient code, and model checkers and proof assistants can use to pick the right theory for SMT solvers. But today we have compilers that compile untyped languages to machine code that's as efficient as that for typed languages (often directly using those partial evaluation results I mentioned). They work by employing speculative unsound abstractions with guards that fall back to interpretation if the guard fails, and then re-compile the code based on a wider abstraction. Unfortunately, I know very little about CEGAR model checking, but from the slogans I get the sense that they work along the same lines, but in the reverse direction: if the abstraction is too wide to prove the requested property, a narrower one is tried. Would it be possible to employ the same technique used by modern partial-evaluation compilers to also widen abstractions in model checkers if the speculative type proves wrong? Just as those state-of-the-art compilers employ a combination of interpretation and compilation, perhaps so could model checkers.

Ron