|
|
|
|
|
|
by zozbot234
665 days ago
|
|
|
> Would it be actually possible to write something like an "a la carte temporal logic library" for other proving languages that could get you some of the confidence you can get from TLA+'s modeling? Temporal logic is just a specific instance of a modal logic, which can be modeled with reasonable ease using a "possible worlds"-based encoding. Note that TLA+ combines temporal logic with non-determinism, which is a different modality. |
|
|