structural vs. language-dependent properties

[adl]

Another suggestion from Joachim.

Most of the properties we list are structural (they depends on the structure of the automaton, e.g., deterministic) while some other might inherent to the language represented by the automaton (e.g. stutter-invariant). It could be useful to partition the set of properties in two to make it clear what is structural and was is language-dependent. This way, a tool processing an automaton without changing its language could propagate all the language-dependent properties that were already specified on input.

We discussed either using a prefix for property names, or (my preference) using two kind of properties: lines.

[kleinj]

I still like this idea. Concrete proposals:

1. language-properties: for language-based properties and properties: for automata properties
2. With prefix: lang-stutter-invariant vs deterministic
3. ...?

I have no strong opinions about the syntax. Besides stutter-invariant, what other language properties would we like to list? Ideas:

• safety: every rejected word has a bad prefix, i.e., a prefix w such that w w' is rejected for all infinite words w'
• liveness: for all finite words w, there is an accepted word w' with prefix w
• universal: language consists of all infinite words
• empty: language is empty

Alexandre, you do property classification in Spot, are there some classifications that we could use here?

[xblahoud]

I prefer syntax 1.

[JanKretinsky]

I don't like the prefixes, Joachim's number 1. is fine

[adl]

I was thinking about this after reading Joachim's email, and I think I'm simply fine with the current situation.

1. we already have tools that, following the current wording of the specifications, build automata with language-dependent properties such as properties: stutter-invariant, and tools that consume it. E.g., ltl2tgba can output properties: stutter-invariant and the development version of ltl2dstar can use it.
2. for all specified properties, it is easy to tell whether they are language-dependent or not
3. we have 0 experience with user-supplied properties

Splitting "properties:" into two headers just for the purpose of being able to handle unknown language properties if they are ever needed, seems to require some changes in our tools and in the format, for no immediate benefits. If you really want to do it, I'll do it as well of course, but my (lazy!) inclination would be not to work on this until we can actually feel it is needed.

Currently, if we want to preserve language-related properties in our tools, we need a hard-coded list of those properties. That is fine with me, as I already have to make explicit decisions in all algorithms about the other non-language-related properties I keep track of.

I also feel like those language properties is only a fraction of the problem. There might be non-language-related properties that are preserved by a transformation, and that tools do not know about. Again, I think we lack experience. If we ever have user-defined properties to preserve, an easy fix for our tools would be to have an option like --keep-prop=foo allowing user to tell: "run your algorithm, but keep the foo property if it was present in the input because that is important to me". The same idea could be applied to unknown headers. Again, I'm not suggesting to implement those options: I'm just saying this is something we can easily do later if we do nothing now.