Notes on "Distributed reactive systems are hard to synthesize"

The original theorem of undecidability of distributed reactive systems appears in  Distributed reactive systems are hard to synthesize. Here I'd like to share some thoughts on the proof sketch presented in the the paper.

Two Flavours of Bounding in Bounded LTL Synthesis

Definitions and context is taken mainly from SF07.

There are two ways to "bound" in bounded synthesis approaches [KV05, SF07, FJR09]. The first one is to bound the size of the module synthesized. The second is to bound the number of visits to a bad state along the run path in the specification graph (informally can be seen as bounding the "reaction time" of the system) (here we count visits to different bad states separately).

Here are the differences:
1. Bounding |Impl| implies bounding |#bad_state_visits|:

|#bad_state_visits| <= |Impl|

2. .. but bounding bounding |#bad_state_visits| does not imply the bound on the implementation |Impl|!

The (2) can be easily seen in the specification: 

G(r -> Fg) & G(x <-> Xy & XXy & ..)

Bounding |#bad_state_visits| does not restrict the size of the implementation which depends on the specification -- the size essentially depends on how many X's we have in the second conjunct, and not on |#bad_state_visits|.

The (1) becomes clear if consider a run graph and a lasso with a bad state inside. The length of the lasso is equal to |bad SCC| * |Impl|. This lasso by definition contains all different pair of states (s_of_impl, s_of_graph), and it starts and closes in the same pair. Therefore the maximum number of visits to the bad state is achieved when all s_of_graph in the lasso are the same and equal to that bad state. Therefore, |#bad_state_visits| is bounded by |Impl|.

It is interesting to see other ways of boundings!