Vai al contenuto| Home page|

   Ti trovi in: HOME »Programmi, progetti e risultati »I progetti »PRIN - Programmi di ricerca di Rilevante Interesse Nazionale»Programma di ricerca
INIZIO_TESTO_DA_INDICIZZARE

RESEARCH PROGRAM

italiano - inglese
Similar research programs:
Scientific and education field classification
International Patent Classification
Geographical classification
Keywords
CONSTRAINTS IN ARTIFICIAL INTELLIGENCE; PREFERENCES; CONSTRAINT PROGRAMMING; CONSTRAINT LOGIC PROGRAMMING; CONSTRAINT SOLVERS

Constraints and preferences as a unifying formalism for system analysis and solution of real-life problems

Università degli Studi di Padova
Abstract
Constraint programming is a multi-disciplinary research area where the fields of research range from Artificial Intelligence, to Operation Research, to Programming Languages, to Databases, and whose applications are present in many disciplines.

Constraint programming is a programming paradigm which is fundamentally different from the others, since it consists of modelling a problem in a declarative way (by stating its "constraints"), and then solving it via general procedures which explore the solution space and prune useless parts by an active use of the constraints. Typical successful applications of constraint programming are scheduling, rostering, vehicle routing, timetabling, and frequency assignment. Newly considered applications are protein folding, online configuration, web searching, and system and program analysis.

Research in the field of constraint programming started in the 70's within Artificial Intelligence, and since 1995 it has seen a significant increase of the theoretical and practical interest, with an annual international conference (CP), an international association (ACP), several workshops and volumes, an international journal, and five books. Europe leads the research in this field, but several groups working on constraint programming are scattered around the world. In Italy, research on constraint programming is done mainly by the groups participating to this project, where one of the main goals is to make these groups communicate and to foster their collaboration, in order to exploit the common skills for an easy communication, but also the complementary skills for a fruitful collaboration which can lead to new theoretical and practical results.

More precisely, the goal of this project is to study extensions of existing formalisms and techniques for constraint programming, with emphasis mainly on innovative applications both on computing systems (such as security and program analysis) and on real-life problems (such as scheduling and bioinformatics). We will thus use constraints as a unifying formalism, and the application domains as the driving force for the extensions of the languages and techniques for solving constraints.

In particular, we will study how to:
-- extend the formalisms to model preferences, to be able to model negative, positive, conditional, qualitative, and quantitative preferences;
-- model and solve multi-agent scenarios, and study their fundamental properties;
-- develop innovative techniques for multi-criteria optimization problems;
-- handle constraints on intervals and sets.

The application domains we will consider are:
-- modelling and solutions of scheduling problems,
-- verification of properties of concurrent systems with infinite states,
-- analysis of multi-level security protocols,
-- bioinformatics.

Each research unit has common skills and knoweldge that up to now has been used mainly separately. The project will allow for the exploitation of both the common and the complementary skills, in order to get innovative results both on theory and on applications. <<<

Principal Investigator
Francesca ROSSI Università degli Studi di PADOVA
Research Objectives
The goal of this project is to study the extension of existing frameworks and techniques for constraint programming, in particular with respect to innovative applications both to formal systems (e.g. security, program analysis) and to real problems (e.g. scheduling, bioinformatics). We will thus use constraints as a unifying approach and the applications as a motivation for the extensions of the languages and of the techniques for constraint solving.

Research units

To achieve this goal, we have gathered some of the main groups in Italy working in this area, in order to exploit the common knowledge for facilitating communication, and the complementary expertise for a fruitful cooperation leading to new theoretical and practical results. Such groups are present in the research field at international level and produce regularly practical and theoretical results which are well accepted by the international research community and which have started new lines of research in constraint programming.

More specifically:

-- unit 1 (Padova), which coordinates this project, has strong competences in soft constraints and preferences as well as in the application of constraint techniques to scheduling problems;

-- unit 2 (Udine) has experience in the definition and development of new logic programming languages with set-based constraints and also in the application of constraint techniques to bioinformatic problems and to hybrid systems analysis;

-- unit 3 (Genova) contributes to this project with its expertise in constraint-based system analysis;

-- unit 4 (Pescara) has a strong knowledge of both the study of logic and concurrent languages based on constraints and of the application of constraints to security related problems.

Added value of the consortium

All the research units have a deep knowledge on constraint techniques, and have devoted their attention to different problems which are however related to each other. The added value of this project is thus represented by the possibility, via a tighter collaboration and meetings oganized during the project, to share competences, even the complementary ones, with the aim to strenghten and improve the results of the single units and to open new perspectives fo the techniques developed in the corresponding applicative fields. We have thus isolated some lines of work which will allow to achieve this and that are also connected to each other in order to facilitate the transfer of results from one line to the other.

Work themes

In particular, we will study:

-- The extension of formalisms for modeling positive and negative, conditional and unconditional, as well as qualitative and quantitative preferences. At present there are many formalisms to describe these different types of preferences, but none which allows to deal with all at once.
Working units: Padova, Pescara.

-- Modeling and solving multi-agent problems, and studying their fundamental properties. This will be a interdisciplinary activity which will use techniques taken from AI and social choice theory.
Working unit: Padova.

-- The development of techniques for handling multi-criteria optimization problems. In this context also OR techniques will be used mainly for their usefulness in optimization problems.
Working units: Padova, Udine.

-- Handling interval-based constraints and (multi)set-based constraints. This line of work will extend the applicability of constraint programming to those environments where it is natural to specify constraints in terms of intervals or sets.
Working unit: Udine, Genova.

The application domains which we will consider are:

-- Scheduling problems.
The goal is to handle problems which featurealso preferences on the activities and where the solution obtained should be robust to changes of the context.
Working unit: Padova.

-- Verification of concurrent and a infinite-state systems.
The aim it to extend the state of the art in this field using constraint techniques and notions of compositionality.
Working units: Genova, Udine, Pescara.

--Multilevel security protocols analysis.
The main goal is to use soft constraints to model more faithfully, and thus for solving in a more satisfactory way, typical problems of security and systems.
Working units: Pescara, Genova.

-- Bioinformatics.
The goal is to develop solvers for specific constraints dedicated to bioinformatics problems, as the prediction of the 3D structure of a protein.
Working unit: Udine. <<<
Timescale
24 months
National and international background
Constraint programming [MS98,D03,Apt03] is a programming methodology which allows one to formalize the problem to solve in a purely declarative way, with the help of logical formulae called constraints. The computation phase is typically based on the search for one or more solutions which satisfy the set of all constraints. Constraint programming allows one to keep the formalization phase and the search for solutions completely separate. However, also the search for solutions is guided by the constraints to be satisfied, in order to significantly reduce the search space.

A constraint solver is an effective procedure that is able to check the satisfiability of constraints and to find solutions which satisfy all of them, if any. Several solvers have been proposed since the 80's, for several constraint domains and with different properties and
implementation techniques. Several of these solvers have been proposed within Constraint Logic Programming (CLP) [JM94], where currently the most widely used systms are SICStus Prolog [SICS] and ECLiPSe [ECLI]
which provide several constraint domains and corresponding solvers, and which have been used with success in the solution of optimization problems or in the search for feasible solutions for problmes with complex domains and with arbitrary objective functions.

The use of constraints over finite domains allows one to define combinatorial optimization problems, such as scheduling problems, timetabling problems, etc. Constraint solver for such domains are based on the concept of constraint propagation, typically using some version of the arc-consistency technique [M77], and on the search in the space of all solutions, guided by constraint propagation which allows one to discover partial variable assignments which cannot lead to feasible solutions. For optimization problems, the well-known branch-and-bound technique is used together with constraint propagation to reduce the number of solutions to check before finding an optimal solution.

In many real-life problems, not all solutions are equally desirable. Moreover, in some situations the constraints are naturally associated to preferences which tells us how important the constraint is, or how bad it is if we violate it. To faithfully model such situations, the classical constraint formalism has been generalized to allow for the description of preferences. Preferences are just constraints where, for each combination of values to the variables of the constraint, it is associated an element (that is, the preference for that combination) taken from an (partially or totally) ordered set. In the last 10 years various formalisms have been developed to model and handle problems with preferences, among which the most general are the one based on semirings [BMR97], the valued CSPs [SFV95], and the so-called CP-nets [BBHP99]. Solving a problem with preferences is in general more complex than solving a constraint problem, since now the desired solutions are only those that are optimal according to the preferences. Techniques of branch-and-bound, of constraint propagation adapted to work with preferences rather than classical constraints, and of abstraction, are useful to build a solver for problems with preferences.

Besides preferences, several real-life problems contain uncertain parts, where the user cannot take decisions but only observe the happening of the events. For this reason, it is important to be able to handle uncertainty in problems with constraints and/or preferences. The goal is then to find one or more solutions which are good according to the preferences but also reasonably compatible with the uncertainty of the problem. Various formalisms to model uncertainty have been used, depending on the kind of uncertainty considered. For example, one can associate a probability to each event, or, when estimates are not available, a degree of possibility [Z78,DFP96].

Multi-objective optimisation is considered important in many real life applications. In combinatorial problems arising from industry or economics, there are typically many aspects that should be optimised, since objectives can be conflicting and it is not always possible to agreggate them into a single objective function. Moreover, objectives can be conflicting and a solution optimal with respect to one objective function could be sub-optimal, or even unacceptably bad with
respect to the others. The problem is very wide and it has been addressed in different research areas: in Artificial Intelligence, in particular in Constraint Programming [G02], and also in Operations Research [EG00]. Multi-objetive optimization is tightly related to
preference aggregation in multi-agent systms, where a preference aggregation function has to decide the best solution for all the agents [RVW04]. In such scenarios, many impossibility rsults have been proven, concerning properties such as fairness and non-manipulability [A51,G73].

Many real-life applications involve time-critical aspects. Characteristic of such applications, usually called real-time embedded systems, is the specification of timing constraints such as, for example, that an input is required within a bounded period of time. In order to model such situations, a language should allow us to specify that, in case a given time bound is exceeded (i.e. a time-out occurs), an alternative action is taken. Many different formalisms have been developed to specify, verify and program reactive systems, including timed process algebras, temporal logics, and concurrent constraint languages such as timed CCP [SJG96,DGM00]. Intervals have a central role in temporal representation and reasoning. Temporal properties of systems developed in different areas, such as planning, natural language processing, definition and verification of hardware and software systems, and Bioinformatics can be naturally formalized using interval-based formalisms. Interval-based temporal-logics represent one of the more interesting systematic approaches to temporal intervals handling [GMS04]. Recently a tableau method for the logics CDT interpreted on partial orders has been proposed in [GMSS05]. This method combines the features of classical tableau methods for first-order logics with explicit tableau methods for modal logics, that include a specific component for handling constraints on labels.

The power of set-based constraints has been investigated as well. Their use allows to design working prototypes for a given problem, at a high level of abstraction. Several results have been obtained in the sets/multisets/hypersets constraint solvers area [DPR98,DPR01]. In addition, a constraint logic programming language CLP(SET) [DPPR00] has been recently designed and implemented. In [DDPR03] the combination of CLP(SET) and CLP(FD) results in a constraint language over various domains that exploits the declarativity of set-based constraints and the efficiency of finite domains constraint solvers. Recently it has been shown that the language CLP(SET) is suitable for modeling and solving security problems [WWJ2004]. Members of the Udine team have also recently developed some traditional languages with set constraints, such as Singleton [R02].

Constraint programming has a wide variety of applications. In this project we plan to study some of these applications and to improve their handling through new techniques which we propose to develop.

1. Scheduling problems

Scheduling problems occur in many real-life situations [OPCC03,RDF05]. In fact, a scheduling problem can be defined as the assignment of start and end times to a set of tasks (or actions), subject to certain constraints. Constraints are typically either time constraints or resource constraints. Coordination of production in a factory, management of space missions, and transportation scheduling are representative examples.

Feasibility alone is seldom the goal of scheduling; in fact usually a set of objectives and preferences have to be optimized. Therefore the scheduling problem is primarily concerned with figuring out when tasks should be executed so that the final solution guarantees good performances.

2. Static analysis and abstract interpretation

By static analysis we mean the collection of techniques which are able to prove program properties at compile time. Abstract Interpretation is a semantic framework for the static analysis of systems, introduced by Patrick and Radhia Cousot in [CC79]. The idea behind abstract interpretation is to compute the formal semantics of a system, either hardware or software, in an abstract domain which is different from the standard one. Each object in the abstract domain represents a set of objects in the concrete domain. Obviously, the result is only an approximation of the real semantics of the system. However, if the abstract domain is appropriate, it may convey all the relevant properties we need. Most of these results have proved useful in the field of static analysis of logic programs, where the standard domain, sets of substitutions, is essentially a constraint system.

3. Symbolic model Checking

The automatic technique known as Model checking has been introduced in [CE81] as an alternative to simulation techniques for validation of hardware design. In this setting the specification of the system properties is given in temporal logic [P81]. Furthermore, a model of the logic of a circuit and of related communication protocols is described using a transition system.

The model checking algorithm terminates successfully if the model satisfies the temporal property, otherwise it returns a counterexample that violates it. Being based on an exhaustive exploration of the state space, the major problem of model checking however is scalability. Recently, however, the application of dedicated data structures for representing sets of states (BDDs) has enlarged the spectrum of the concurrent systems to which model checking can be applied. Symbolic model checking [BCB+90] implements this technique.

The first applications of model checking have been studied for the logical models of hardware systems, i.e., finite-state systems. In recent years may efforst have been spent to extended (symbolic) model checking to system with an infinite-state space [AH92,MCJ97,ACJT96,ACH+95,AJ03].

The main ideas underlying model checking can naturally be extended to systems with an infinite-state space. In most of the extensions of model checking to infinite-state systems, the key concept is the use of constraints as a symbolic representation of infinite sets of states. In this setting constraints are used as an assertional language [KMMPS01] to represent infinite collections of system configurations. Constraint operations are then use to symbolically manipulate sets of states within the fixpoint based algorithms underlyinhg model checking.

Another approach to the verification of infinite-state systems, which is automatic although incomplete, uses logic programming with constraints to specify reactive systems and their properties, as well as the specialization of programs as an inference mechanism for verifying the properties of interest. With these techniques, properties of safety and liveness have been proved for various infinite-state protocols [FPP02,FPP04].

In the last years constraint-based verification has found several practical applications. In most of these applications constraint-based verification is combined with abstractions defined both at the specification level [D00,DB01] and at the level of symbolic representation of sets of states [BD02a].

One of the most interesting research directions for the applications of constraints to verification of infinite-state systems concerns the study of systems with heterogenous data and working in open environments. In this setting it seems important to study the combination of constraints with compositional verification techniques and with verification techniques based on game theory.

4. Verification of hybrid systems

Hybrid Automata were first introduced in [ACHH92] as a model and specification language for hybrid systems, i.e., systems consisting of a discrete program within a continuously changing environment. Since their introduction, they have been widely used for the automatic verification of both engineering and biological systems.

A state of a hybrid automaton is specified by providing a state of the discrete component and an assignment for the continuous variables. The problem is that of characterizing the set of states reachable through continuous and discrete transitions from the initial states.

Recently, symbolic methods based on the translation of the automaton into constraints (formulae) over the reals and on the development of specific constraints solvers in the study of hybrid automata emerged. Such approaches exploit Tarski's decidability result for the first-order theory over the real numbers [T51]. Recently, [RS05] has suggested a new constraint propagation based abstraction refinement for the safety verification of hybrid systems with autonomous differential equations.

5. Security

The security of a network configuration is based not just on the security of its individual components and their direct interconnections, but also on the potential for systems to interoperate indirectly across network routes. Such interoperation has been shown to provide the potential for cascading paths that violate security, in a circuitous manner, across a network. In [BFO04] it is demonstrated how constraint programming provides a natural approach to expressing the necessary constraints to ensure multilevel security across a network configuration. In particular, soft constraints can be used to detect and eliminate the cascading network paths that violate security and to obtain a minimal solution (even if not optimal) in polynomial time. Soft constraints can also be effective in improving the analysis of integrity policies [BF03a,BF03b].

6. Bioinformatics

Recently, various Bioinformatics problems have been shown to be successfully implemented as problems over Finite Domains [CB01]. In detail, the problem of determining the three dimensional conformation of a specific protein, whose sequence of composing aminoacids is known (Protein Folding), has been modeled over a discrete domain (Face Centered Cube) in [BW01] using approximated energy functions (HP model).

The protein folding problem is tackled in the literature by various methods, mainly simulations. These programs consider the interactions among the atoms that form the protein. The thermodynamic laws encoded are precise as well as computation-intensive.

Recently, it has been shown how to naturally design Concurrent Constraint Programming programs for simulation, where the base elements are concurrent processes associated to each aminoacid in the protein [DDF04a]. <<<