In this paper we propose a behavioural model, namely the Extended Modal Labeled Transition Systems, as a basis for the formalization of the different notions of variability usually present in product families definitions. In particular, an EMLTS is able to define a family of products by telling at any state of the system whether transitions are optional or compulsory for the products of the family. Based on this model, verification that a product belongs to a family can be carried out by means of automatic tools. Categories and Subject Descriptors D.2 [Software]: Software Engineering; D.2.1 [Software Engineering]: Requirements/Specifications--Methodologies; D.2.4 [Software Engineering]: Software/Program Verification--Formal methods General Terms Theory, Verification, Design Keywords Software families, product lines, modal transition systems