Verication of External Specications of Reactive Systems