The ubiquitous use of computerized systems, and their increasingcomplexity, demand formal evidences of their correctness. Whilecurrent formal-verification techniques have already been applied to anumber of case studies, they are not sufficient yet to fully analyzeseveral aspects of complex systems such as communication networks,embedded systems or industrial controllers. There are three importantcharacteristics of these systems which need to be tackled:- the rich interaction that crucially constrains the behaviour ofsuch systems is poorly taken into account in the actual models;- the imprecisions and uncertainty inherent to systems that areimplemented (e.g. on a digital processor), or which interact via anetwork, or which control physical equipments, are mostly ignoredby the verification process;- the deployment of large interacting systems emphasizes the lack fora modular approach to the synthesis of systems.The goal of this project is to develop a systematic approach to theformal analysis of interacting systems. We will use models from gametheory for properly taking into account the interaction in thosesystems, and will propose quantitative measures of correctness andquality, that will take into account the possible perturbations in thesystems. The core of the project will be the development of variousalgorithms for synthesizing high-quality interactive systems. We willbe particularly attached to the modularity of the approach and to thedevelopment of efficient algorithms. The EQualIS project will deeplyimpact the design and verification of interacting systems, byproviding a rich framework, that will increase our confidence in theanalysis of such systems.