Model checking properties on reduced trace systems