Re: [tlaplus] Verifying fairness | TLC Errors | Refinement

On 25 Oct 2021, at 03:18, Jones Martins <jonesmvc@xxxxxxxxx> wrote:

Hi everyone,

Thank you, Andrew, Stephan, Travis, and Markus for your responses!

I'd like to clarify some of these questions:

1) I asked this question because I'm still confused by how WF and SF works (currently, I differentiate them by thinking a WF action has lower priority than an SF action). This confusion led me to find the formal definition of WF and SF in the Hyperbook.
Am I right in saying that verification means “breadth-first searching” a state graph until TLC finds a counterexample is found?

TLC explores the state graph in a breadth-first search. When it encounters a state that violates an invariant, it reports the invariant violation and stops. (Temporal) properties are evaluated periodically during the construction of the state graph and again at the end when the entire graph has been computed, so it is not guaranteed that TLC will stop at the earliest possible point, and counter-examples to temporal properties are also not guaranteed to be of minimal length.

If so, when we search for properties of the form “<>P”, are we saying “There's at least one state in the state graph where P is true, and this spec reaches that state eventually”?

We are saying "Every behavior that satisfies Spec has a suffix for which P is true". If P happens to be a state predicate, then this is the same as saying "Every behavior that satisfies Spec will eventually reach a state where P is true".

Now, for invariants of the form “[]P”, are we saying “P is true for all states of a state graph”?

Yes, if P is a state predicate. In general, it means "Every suffix of any behavior satisfying Spec must satisfy P".

And if those are true, how does TLC deal with composition of operations, such as <>[]?
Would you have any book or article recommendations expanding on that?

Unlike CTL model checking, LTL / TLA model checking doesn't work by recursively checking the sub-formulas of a formula, and in fact it doesn't make sense to say that a state satisfies a property of the form []P since temporal formulas are evaluated over sequences of states, not states. Markus already provided pointers to the literature, the textbooks by Baier/Katoen [1] and by Clarke, Grumberg et al. [2] are probably the most comprehensive ones.

2) My mistake. I meant temporal properties. It seems to me an optimization trade-off, as Markus pointed out.
I believe finding refinement errors is also rather difficult, but for separate reasons.
It sounds like an interesting challenge. Although I don't think I'm ready for it, I'd like to read his pointers.

4) My main concern is what is an abstraction (refinement). In my example above I mention 3 specifications, but my explanation is confusing.
Here's an example:
I am currently dealing with a very simple Bully election algorithm.
The most abstracted version (called SpecA) contains three variables:
- IsActive (mapping for each processor),
- Leader (what process is leader),
- PC (system state).
All three variables change in all states.

Init == ...
Next == \E p \in Procs: (ProcessActivates /\ ElectionWhenActivated) \/ (ProcessDeactivates /\ ElectionWhenDeactivated)
Spec == Init /\ [Next]_vars /\ Liveness

Now I'm writing SpecB, where elections (should) happen AFTER a process' status changes instead of immediately.

Would it be possible to SpecB implement SpecA? Or not, it's impossible because three variables always need to change together even in Spec2, Spec3, and so on...

If the activation status of processes and the leader (i.e., the result of election) are externally observable and your high-level spec says that election happens immediately when the activation status changes then refinements must also do this. Otherwise, an external observer could detect a difference between the behavior of the low-level system (where first the activation status changes and later a process is elected) and the high-level system (where the two happen simultaneously). For example, you might prove an invariant of the high-level spec that asserts that the leader is always active, and that invariant could be violated in the lower-level spec where the current leader gets deactivated before a new leader is elected. Refinement preserves all properties.

Hope this helps,

Stephan

[1] https://mitpress.mit.edu/books/principles-model-checking

[2] https://mitpress.mit.edu/books/model-checking-second-edition

Thank you very much.

Regards,
Jones Martins

On Thursday, 21 October 2021 at 19:09:40 UTC-3 Markus Alexander Kuppe wrote:

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/121ff5a5-5dcc-479a-8f8c-ecbd9d1e1606n%40googlegroups.com.

Re: [tlaplus] Verifying fairness | TLC Errors | Refinement | Verifying properties