Re: logics for model checking