Disclaimer
	• The intent of this work was to evaluate symbolic model checking of state-based specifications, not to evaluate the TCAS II specification.  Our study used a preliminary version of the specification, version 6.00, dated March, 1993.  We did not have access to later versions, so we do not know if the issues identified here are present in later versions.