Семинар 10

1) Убедитесь в эквивалентности следующих формул LTL:

Двойственность \(\mathrm F\) и \(\mathrm G\):
- \(\neg\mathrm G\,\phi\equiv\mathrm F\,\neg\phi\)
- \(\neg\mathrm F\,\phi\equiv\mathrm G\,\neg\phi\)
Двойственность \(\mathrm U\) и \(\mathrm R\):
- \(\neg(\phi \,\mathrm U\,\psi)\equiv\neg\phi\,\mathrm R\,\neg\psi\)
- \(\neg(\phi \,\mathrm R\,\psi)\equiv\neg\phi\,\mathrm U\,\neg\psi\)
Дистрибутивность:
- \(\mathrm F\, (\phi\lor\psi)\equiv \mathrm F\,\phi\lor \mathrm F\,\psi\)
- \(\mathrm G\, (\phi\land\psi)\equiv \mathrm G\,\phi\land \mathrm G\,\psi\)
Выразимость \(\mathrm F\) и \(\mathrm G\):
- \(\mathrm F\,\phi\equiv \top\,\mathrm U\, \phi\)
- \(\mathrm G\,\phi\equiv \bot\,\mathrm R\, \phi\)
Выразимость \(\mathrm U\) и \(\mathrm W\):
- \(\phi\,\mathrm U\,\psi\equiv\phi\,\mathrm W\,\psi\land\mathrm F\,\psi\)
- \(\phi\,\mathrm W\,\psi\equiv\phi\,\mathrm U\,\psi\lor\mathrm G\,\phi\)
Выразимость \(\mathrm W\) и \(\mathrm R\):
- \(\phi\,\mathrm W\,\psi\equiv\psi\,\mathrm R\,(\phi\lor \psi)\)
- \(\phi\,\mathrm R\,\psi\equiv\psi\,\mathrm W\,(\phi\land \psi)\)

2) Обоснуйте адекватность следующих множеств темпоральных связок в LTL: