An efficient verifier of truly concurrent properties