search

gaperez64 / acacia-bonsai

A minimal implementation of reactive synthesis via universal co-Buchi automata using antichains
GNU General Public License v3.0
4 stars 3 forks source link

Unreal cores #24

Closed gaperez64 closed 1 year ago

gaperez64 commented 1 year ago

Suppose the realizability algorithm said the spec is unrealizable for a given k. Can we output an "unrealizability core" in the spirit of unsat cores from SAT? Perhaps we can even have some sufficient conditions for UNREAL with low k values to imply actual unrealizability?

This was proposed by A. Cimatti.

gaperez64 commented 1 year ago

A naive choice of unreal core is the strategy of the adversary. Can we leverage with low K-values to say something? That would save us the need to check the complementary game with the same K or, even worse, having to increase the value of K.

I don't see this as a priority anymore as the value of K is usually quite low for most benchmarks we've encountered.