Analysis of model-based specifications
	• Given a model-based (Z-like) specification, can we determine if it is inconsistent? • In particular, can we do for Z-like specifications what we did for model checking: determine if something is not true that we expect to be true