Towards first-order symbolic trajectory evaluation using MDGs