Re: [tlaplus] Existential quantifiers over behaviors for temporal properties?

Hi Andrew,

let’s be really precise (since that’s what TLA+ is about): it's not the temporal operators that universally quantify over behaviors but the definition of validity. A formula of temporal logic is evaluated over an individual behavior, but we say that a specification Spec has a property Prop if the implication Spec => Prop is valid, i.e., holds for all behaviors. This is very different from saying that if all behaviors satisfy Spec (which will not be the case) then all behaviors satisfy Prop.

As you certainly know, branching-time logics such as CTL or CTL* offer connectives that quantify over (suffixes of) behaviors, and you could express reachability of an accepting state using a formula such as E<> accepting. Formulas are then evaluated over computation trees rather than linear behaviors, and the above formula holds if the tree contains a branch that contains a state satisfying the predicate `accepting’. There was a huge debate on the relative merits of linear-time and branching-time logics in the 1980s and 1990s, and it’s not necessary to repeat the arguments.

You also know that a reachability property such as the one that you describe can be checked in a linear-time formalism using inverted logic – that is, by asserting the invariant that an accepting state is never reached (in any run of the automaton for the given input string, or equivalently that no application of the CFG rules matches the string), and expecting the model checker to produce a counter example, which exhibits an accepting run / sequence of rule applications. Why is this approach unsuitable for what you are after?

Stephan

On 15 Oct 2024, at 16:25, Andrew Helwer <andrew.helwer@xxxxxxxxx> wrote:

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.

--
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/BE0249E6-60BB-4E4D-B137-94A70C3A9313%40gmail.com.