• Modal Transition System
• Product Family
• Deontic Logic
• Model Checking

Product Lines or Families represent a new paradigm widely used to describe company products with similar functionality and requirements in order to improve efficiency and productivity of a company. In this context many studies are focused on the research of the best behavioural model useful to describe a product family and to reason about properties of the family itself. In addition the model must allow to describe in a simple way different types of variability, needed to characterize several products of the family.
One of the most important of these models is the Modal Transition System (MTS), an extension of a Labelled Transition System (LTS), which introduces two types of transitions useful to describe the necessary and allowed requirements. These models have been broadly studied and several its extensions have been described. These extensions follow different approaches which entail the introduction of more and more complex and expressive requirements. Furthermore MTS and its extensions define a concept of refinement which represents a step of design process, namely a step where some allowed requirements are discarded and other ones become necessary.
In this thesis we introduce a new model, the Constrained Modal Transition System (CMTS ), which is a particular and more expressive extension of MTS. Moreover we study different and useful properties correlated to the CMTS. Also, we use CMTS as an useful tool to determine and to define a a hierarchy of expressivity of the known extensions with variability of LTSs and MTSs. In order to check different properties of a product family, we introduce a new deontic-temporal logic based on CTL* interpreted over CMTSs able to express classical safety and liveness properties as well as concepts like obligatory, permission and prohibition. Finally some useful optimizations are introduced to guarantee a less expensive verification from complexity point of view.