Allow analysis for missing/removed states/transitions in data-based synthesis result
We have an event-based synthesis analysis tool already, but lack this for data-based synthesis. I recently stumbled upon a paper that explains how to do this for symbolic synthesis (using the same algorithm we use in data-based synthesis:
- L. Swartjes, M.A. Reniers and W.J. Fokkink, "Deducing causes for the absence of states in supervised systems", 6th International Conference on Control, Decision and Information Technologies (CoDIT), pages 144-149, 2019, doi:10.1109/CoDIT.2019.8820346.
I think this would be a very valuable addition to CIF. It would allow debugging/diagnosing/analyzing the result of data-based synthesis, making it less of a magic black box.
Some thoughts relating to adding this to CIF:
- The algorithm in the paper only supports state-based requirements, and not for instance requirement automata, although it suggests a way to do a conversion. Needs to be looked at in detail.
- The algorithm in the paper only allows deterministic transition relations. Not sure what is needed to make it support non-deterministic transition relations. We could start with only deterministic models if we enable this analysis.
- The algorithm in the paper assumes all states are reachable in the plant. I think we could see what the plant already disables, as an extension.
- The algorithm in the paper assumes no unreachable states in the supervised system. It thus requires forward reachability be enabled. This makes sense current already when one desired better understandable synthesis results.
- I wonder how easy it would be to implement this algorithm.