Транслятор автоматной модели во входной язык верификатора SMV