Expand VTS scope to TLC liveness checking

[lemmy]

Extend the VTS to include liveness-checking in addition to safety. This requires foundational/conceptual work to define an appropriate validation strategy for TLC’s liveness checking. Unlike safety validation, liveness cannot currently be tested by comparing TLC and Apalache outputs, because Apalache does not support liveness checking.

Potential approaches to evaluate:

1. Reduce liveness to safety

• Investigate whether a liveness-to-safety transformation can be used as the basis for VTS tests (cf. Liveness to safety reduction and prior Apalache-related work).
• Assess whether this is sufficient for the full range of TLA+ liveness features. Known concern: this may not adequately cover more advanced TLA+ liveness properties, especially properties over actions.

2. Implementation-level assurance for TLC liveness

• Explore a more technical/formal route focused on establishing correctness of TLC’s liveness-checking implementation itself, rather than relying only on behavioral differential testing (as is done for safety).
• This would likely require a different qualification argument than the current VTS approach.

3. Behavioral testing using TLAPS (emerging option)

• Evaluate whether recent/ongoing TLAPS support for proving liveness properties could enable a behavioral-testing strategy analogous to the current safety validation workflow. If viable, this may provide an oracle or reference basis for liveness test cases.

Outcome needed: a documented validation strategy (or combination of strategies) for qualifying liveness checking in the VTS, with explicit coverage limits and rationale appropriate for safety-critical qualification contexts (e.g., ISO 26262).

/cc @konnov