Звено от junction к choice не обладает действиями, поэтому склеивая звенья-половинки (и действия на них) получим те же действия, что и на другой половинке.
Звено от junction к choice не обладает сторожем, что равносильно постоянной ИСТИНЕ, поэтому склеивая звенья-половинки и перемножая сторожей получим того же сторожа, что и на другой половинке.

Дело не в склеивании как таковом. При удалении junction мы вместо одного сложного перехода получаем несколько простых, решенных статически. Тут так не удастся: либо создастся дубль choice со звеном одновременно входящим и выходящим из него (и это будет его единственный вход); либо создастся бесконечное количество "простых" переходов: с одним, с двумя, с тремя, ... с N, ... choice'ами без "рефлексивного звена". Отвечая я мысленно дорисовываю действия к Вашему примеру, т. к. обеднённый частный случай, к. м. к. не показателен.   

А возможны ли недостижимые вершины для well formed? Понимаю, что инструмент (типа EA) их должен поддерживать - как иначе сохранить промежуточный результат работы над диаграммой/моделью, но в конечном результате им нет места!

Разрешено всё, что не запрещено.) Я не знаю. Мне кажется, в попытках определять ill- и well formed создатели стандарта UML пока не преуспели.

Дело не в склеивании как таковом. При удалении junction мы вместо одного сложного перехода получаем несколько простых, решенных статически. Тут так не удастся: либо создастся дубль choice со звеном одновременно входящим и выходящим из него (и это будет его единственный вход); либо создастся бесконечное количество "простых" переходов: с одним, с двумя, с тремя, ... с N, ... choice'ами без "рефлексивного звена". Отвечая я мысленно дорисовываю действия к Вашему примеру, т. к. обеднённый частный случай, к. м. к. не показателен.

Попробуем разбираться по шагам.

• Во вложении эквивалентные конструкции?
• Эквивалентность сохраняется, если вместо state1, state2, state3 использовать псевдосостояния choice и junction?
• Эквивалентность сохраняется, если какие-то из state1, state2, state3 представляют собой одну и ту же вершину?

Разрешено всё, что не запрещено.) Я не знаю. Мне кажется, в попытках определять ill- и well formed создатели стандарта UML пока не преуспели.

Может пришло время явно обозначить, что речь идет не столько о том, что есть в стандарте, как о том, что там должно быть.
Можно применить аналогию: Заказчик составил материал, в котором, по его мнению, есть всё необходимое для Разработчика, но на самом деле предстоит  с помощью Аналитика получить новый материал, где действительно будет всё необходимое для Разработчика.

1. Да, по стандарту.

2. Нет. Если State1 и/или State2 -- junction'ы, то прежде следует преобразовывать их. Если State1 и/или State2 -- не junction'ы, и State3 -- choice, то [если мы верим в одновходовые choice] State3 дублируется State3bis и мы получаем:
State1 --[guard1 && guard2]/act1, act3-->State3--> [тут ветки State3]
State2 --[guard2 && guard3]/act2, act3-->State3bis--> [тут ветки State3]

3. Если State2 = State3 и эта вершина choice, то мы получаем:
State1 --[guard1 && guard2]/act1, act3-->State3--> [тут нерефлексивные ветки State3]
к State3 дорисовываем дополнительную ветку, соответствующую одному витку цикла:
State3 --[guard2 && guard3]/act2, act3-->State3bis--> [тут нерефлексивные ветки State3]
к State3bis дорисовываем дополнительную ветку, соответствующую двум виткам цикла:
State3bis --[guard2 && guard3]/act2, act3-->State3bisbis--> [тут нерефлексивные ветки State3]
к State3bisbis дорисовываем ...
т. е. выращиваем бесконечное дерево переходов-звеньев.
Это если придерживаться духа стандартных примеров по использованию junction и choice.
Либо, как предлагалось, превращаем choice в обычное состояние.

Диаграмма состояний описывает работу некоторого исполнителя. В этом можно увидеть повод для аналогий со стандартами языков программирования. Там устанавливаются правила, делающие бессмысленными (ошибочными) некоторые конструкции. Но в программах, составленных по этим правилам могут быть другие бессмысленные места: мертвый и/или недостижимый код. С такой точки зрения, недостижимые фрагменты диаграммы состояний, записанные по стандарту UML, допустимы.

1. Да, по стандарту.

2. Нет. Если State1 и/или State2 -- junction'ы, то прежде следует преобразовывать их. Если State1 и/или State2 -- не junction'ы, и State3 -- choice, то [если мы верим в одновходовые choice] State3 дублируется State3bis и мы получаем:
State1 --[guard1 && guard2]/act1, act3-->State3--> [тут ветки State3]
State2 --[guard2 && guard3]/act2, act3-->State3bis--> [тут ветки State3]

3. Если State2 = State3 и эта вершина choice, то мы получаем:
State1 --[guard1 && guard2]/act1, act3-->State3--> [тут нерефлексивные ветки State3]
к State3 дорисовываем дополнительную ветку, соответствующую одному витку цикла:
State3 --[guard2 && guard3]/act2, act3-->State3bis--> [тут нерефлексивные ветки State3]
к State3bis дорисовываем дополнительную ветку, соответствующую двум виткам цикла:
State3bis --[guard2 && guard3]/act2, act3-->State3bisbis--> [тут нерефлексивные ветки State3]
к State3bisbis дорисовываем ...
т. е. выращиваем бесконечное дерево переходов-звеньев.

Одновходовость choice - это единственная причина необходимости State3bis и т.п. или есть ещё и другие?

Диаграмма состояний описывает работу некоторого исполнителя. В этом можно увидеть повод для аналогий со стандартами языков программирования. Там устанавливаются правила, делающие бессмысленными (ошибочными) некоторые конструкции. Но в программах, составленных по этим правилам могут быть другие бессмысленные места: мертвый и/или недостижимый код. С такой точки зрения, недостижимые фрагменты диаграммы состояний, записанные по стандарту UML, допустимы.

А можно считать ошибкой недостижимость фрагментов диаграммы состояний, хотя бы из соображений минимизации диаграммы. Некоторые так и предлагают http://www.softcraft.ru/auto/switch/umlswecl/umlswecl.pdf стр.7-9

К многовходовости и циклам choice: http://matlab.exponenta.ru/stateflow/book1/3.php (правда это не UML).

Другой причины для дублирования кроме одновходовости пока не придумывается.

Вообще говоря, то, что у них запрещается недостижимое -- это то ли жлобство, то ли педагогическая заморочка. Даже если сгенерить код по недостижимому, то всё будет работать точно также. "Мертвечину", если что, подберёт компилятор языка программирования. Тут какая-то "изюминка" -- вроде, наша среда может обучать составлению "правильных" диаграмм состояний.

Конечно, если диаграмма рисуется для чтения человеком, то "мертвое" лучше с неё убрать.

Ссылка на Матлаб прекрасна. Там и про history junction замечательно написано. Только переводчик ленивый.) Пример без действий, и локальный переход может быть нелокальным -- смысл не меняется. Есть полный пример с действиями: http://info.eps.surrey.ac.uk/SCS/manuals/matlab65/toolbox/stateflow/semant35.html#1028350
Ну и "вкуснятинка" вроде того, что "вертолётной площадки" достаточно, переход в неё может не вести, любой переход к границе суперсостояния на самом деле ведёт к ней (если история не пуста).
И это не choice'ы, это такие junction'ы.) Цикл отработает до выхода из состояния)): http://info.eps.surrey.ac.uk/SCS/manuals/matlab65/toolbox/stateflow/semant40.html
Их можно ставить всюду, даже после начального псевдосостояния. Начальных может быть несколько: http://info.eps.surrey.ac.uk/SCS/manuals/matlab65/toolbox/stateflow/semant31.html
А иногда их можно использовать для того, чтобы вернуться назад как ни в чём не бывало: http://info.eps.surrey.ac.uk/SCS/manuals/matlab65/toolbox/stateflow/semant45.html

И это не choice'ы, это такие junction'ы.

Для меня если условие на исходящем звене проверяется не заранее, а по достижении, то это по сути - choice.

Для меня если условие на исходящем звене проверяется не заранее, а по достижении, то это по сути - choice.

Я так поняло, что если бы были действия (transition action) на циклическом звене, то цикла бы было как бы два. Сначала перед выходом из состояния ходили бы и считали в уме круги, а уж потом бы вышли и сколько насчитали, столько бы раз запустили transition action. Жуткий гибрид.)