[tlaplus] Existential quantifiers over behaviors for temporal properties?

[Andrew Helwer <andrew.helwer@xxxxxxxxx>]

All the temporal operators we have ([], <>, ~>) implicitly quantify over all behaviors generated by a spec. So when we check  really what we are saying

<>P

really what we are checking is roughly:

\A behavior \in BehaviorsOf(Spec) : \E state \in behavior : P

But what if I only care that at least one behavior generated by the spec satisfies <>P? Something like:

\E behavior \in BehaviorsOf(Spec) : \E state \in behavior : P

Currently, you can only do this by tracking nondeterministic system behaviors in a variable contained within the spec itself, then writing a universally-quantified temporal operator over the value of that variable. However, it would be interesting if this could be offloaded to the model-checker.

This idea was inspired by me specifying nondeterministic finite automatons and context-free grammars as part of an experiment in using TLA+ for undergraduate computer science coursework. A CFG accepts a given string w if some application of the grammar production rules results in string w. If I wanted to model-check to ensure a given CFG accepts a string w, I would need to say that there exists some behavior by the CFG resulting in a string composed entirely of terminals and matching w.

What do people think?

Andrew Helwer

-- 
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/efa1d2e9-85d3-4a44-a563-c18832cf23cfn%40googlegroups.com.