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

Thank you for the detailed reply, Stephan. This is connected to two further things; one is the proposed REACHABLE invariant type feature, which obviates the need for the inverted logic you described (although this was not originally conceived as a temporal property): https://github.com/tlaplus/tlaplus/issues/860#issue-2075413374

The second is my recent question about sweeping constant parameters in TLC: https://groups.google.com/g/tlaplus/c/sRyhji5vnX8/m/6Lih_Oc7AwAJ

I don't want to just check whether a given CFG or NFA accepts a single string; instead, I would like to generate a ton of strings over an alphabet in the initial state then run the CFG or NFA on them. I then use refinement to see whether these complicated automata correctly implement the language I think they do, by seeing whether they refine a simple two-state automaton which transitions from the start state to the accept state only if the given string is accepted by the language. So, unfortunately the inverted logic approach would not work in this case, and I don't know that the REACHABLE invariant type would work either.

Andrew

On Tue, Oct 15, 2024 at 10:44 AM Stephan Merz <stephan.merz@xxxxxxxxx> wrote:

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 a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/HwrzMsyfhRU/unsubscribe.
To unsubscribe from this group and all its topics, 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.