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

PROGRAMMA DI RICERCA 2005

italiano - english
Unità di Ricerca
Programmi di ricerca simili:
Classificazione scientifico-disciplinare
Classificazione brevettuale
Classificazione geografica
Bibliografia
[A03] K. Apt. Principles of Constraint Programming. Cambridge University Press, 2003.

[ACH+95] R. Alur, C. Courcoubetis, T. A. Henzinger, N. Halbwachs, P. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. The algorithmic analysis of hybrid systems. TCS 138:3-34, 1995.

[ACHH92] R. Alur, C. Courcoubetis, T. A. Henzinger, and P. H. Ho.
Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems. Hybrid Systems, LNCS 736:209-229, 1992.

[ACJT96] P. A. Abdulla, K. Cerans, B. Jonsson, and Y.-K. Tsay. General Decidability Theorems for Infinite-state Systems. LICS 96, 1996.

[AH92] R. Alur and T. A. Henzinger. Logics and models of real time: a survey. Real Time: Theory in Practice, 1992.

[AJ03] P. Abdulla, B. Jonsson. Model checking of systems with many identical timed processes. TCS 290(1): 241-264,2003

[A51] K. Arrow. Social Choice and Individual Values. John Wiley and Sons, 1951.

[BD02a] M. Bozzano, G. Delzanno. Algorithmic Verification of Invalidation-Based Protocols. CAV 02: 295-308

[BBHP99] C. Boutilier, R. I. Brafman, H. H. Hoos and D. Poole. Reasoning With Conditional Ceteris Paribus Preference Statements.
Fifteenth Conference on Uncertainty in Artificial Intelligence (UAI 1999), pages 71-80. Morgan Kaufmann 1999.

[BCB+90] J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and J. Hwang. Symbolic Model Checking: States and Beyond. LICS 90, 1990.

[BF03a] S. Bistarelli and S. Foley. Analysis of integrity policies using soft constraints. In Proc. of IEEE Workshop Policies for Distributed Systems and Networks, pages 77-80, June 2003.

[BF03b] S. Bistarelli and S. Foley. A constraint based framework for dependability goals: Integrity. In Proc. of 22nd International Conference on Computer Safety, Reliability and Security (SAFECOMP2003), volume 2788 of Lecture Notes in Computer Science, pages 130-143. Springer, 2003.

[BFO04] S. Bistarelli, S. N. Foley, and B. O'Sullivan. Modelling and detecting the cascade vulnerabiliy problem using soft constraints. Proc. ACM Symposium on Applied Computing (SAC 2004), 383-390. ACM Press, 2004.

[BMR97] S. Bistarelli, U. Montanari and F. Rossi. Semiring-based Constraint Solving and Optimization. Journal of the ACM, Vol. 44, No. 2, pages 201-236, 1997.

[BW01] R. Backofen and S. Will. Fast, constraint-based threading of HP-sequences to hydrophobic cores. CP'01, LNCS 2239:494-508, 2001.

[BXS04] T. Bultan, X. Fu, J. Su. Tools for Automated Verification of Web Services. ATVA 2004: 8-10, 2004.

[CB01] P. Clote and R. Backofen. Computational Molecular Biology: An Introduction. John Wiley & Sons, 2001.

[CC79] Cousot, P. and Cousot, R. Systematic design of program analysis frameworks. POPL '79. ACM Press, 269-282, 1979.

[CE81] E. M. Clarke and E. A. Emerson. Synthesis of synchronization skeletons for branching time temporal logic. Ws. Logic of Programs, 1981.

[DDF04a] A. Dal Pal, A. Dovier, F. Fogolari. Protein Folding Simulation in CCP. ICLP 2004, LNCS 3132, 2004.

[D03] R. Dechter. Constraint Processing. Morgan Kaufmann, 2003.

[D00] G. Delzanno. Automatic Verification of Parameterized Cache Coherence Protocols. CAV 00, 2000.

[DB01] G. Delzanno and T. Bultan. Constraint-based Verification of Client-Server Protocols. CP 01, 2001.

[DFP96] D. Dubois, H. Fargier, H. Prade. Possibility theory in constraint satisfaction problems: handling priority, preference and uncertainty. Applied Intelligence, 6, 287-309, 1996.

[DGM00] F. S. de Boer, M. Gabbrielli, and M. C. Meo. A Timed CCP Language. Information and Computation, 161(1):45-83, 2000.

[DP88] D. Dubois and H. Prade. Possibility Theory. Plenum Press, 1988.

[DPPR00] A.Dovier, C.Piazza, E.Pontelli, G.Rossi. Sets and Constraint Logic Programming. ACM Toplas, 22(5) 2000, 861-931.

[DPR98] A. Dovier, A. Policriti, and G. Rossi. A Uniform Axiomatic View of Lists, Multisets, and Sets, and the Relevant Unification Algorithms. Fundamenta Informaticae 36(2/3):201-234, 1998.

[DPR01] A. Dovier, E. Pontelli, and G. Rossi. Constructive Negation and Constraint Logic Programming with Sets. New Generation Computing 19(3):209-255, 2001.

[ECLI] ECLiPSe, User Manual. Tech. rep., Imperial College, London. August 1999. Available at www.icparc.ic.ac.uk/eclipse.

[EG00] M. Ehrgott and X. Gandibleux. A survey and annoted bibliography of multiobjective combinatorial optimization. OR Spektrum, 22:425-460, 2000.

[FPP02] F. Fioravanti, A. Pettorossi, and M. Proietti. Verification of sets of infinite state systems using program transformation. Proc. LOPSTR 2001, LNCS 2372, pp. 111-128. Springer, 2002.

[FPP04] F. Fioravanti, A. Pettorossi, and M. Proietti. Automatic Proofs of Protocols via Program Transformation. MSRAS '04, June7-9, 2004, Poland, 2004.

[G02] M. Gavanelli. An algorithm for multi-criteria optimization in CSPs. ECAI02, 136-140, IOS Press, 2002.

[G73] A. Gibbard. Manipulation of Voting Schemes: A General Result.
Econimetrica, 41, 3, 587-601, 1973.

[GMS04] V. Goranko, A. Montanari, and G. Sciavicco. A road map of interval temporal logics and duration calculi. J. of Applied Non-Classical Logics, 14(1-2):9-54, 2004.

[GMSS05] V. Goranko, A. Montanari, P. Sala, and G. Sciavicco. A general tableau method for propositional interval temporal logics. J. of Applied Logic, 2005.

[KMMPS01] Y. Kesten, O. Maler, M. Marcus, A. Pnueli, E. Shahar Symbolic model checking with rich assertional languages. TCS 256(1-2): 93-112, 2001.

[JM94] J. Jaffar and M. J. Maher. Constraint Logic Programming: A Survey. J. of Logic Programming, 19/20:503-581, 1994.

[M77] A.K. Mackworth. Consistency in Networks of Relations. AI Journal, v.8, 99-118, 1977.

[MCJ97] W. Marrero, E. M. Clarke, and S. Jha. Model Checking for Security Protocols. Technical Report CMU-SCS-97-139, CMU, 1997.

[MR04] M. Milano and A. Roli. MAGMA: A Multiagent Architecture for Metaheuristics. IEEE Trans. on Systems, Man and Cybernetics - Part B, 34(2), 2004.

[MS98] K. Marriott and P. J. Stuckey. Programming with Constraints. MIT Press, 1998.

[OPCC03] A. Oddi, N. Policella, A. Cesta, and G. Cortellessa. Generating High Quality Schedules for a Spacecraft Memory Downlink Problem. Proceedings of CP03, 2003.

[P81] A. Pnueli. A temporal logic of concurrent programs. TCS 13:45-60, 1981.

[R02] G. Rossi. Set-based Nondeterministic Declarative Programming in SINGLETON. Proc of 11th WFLP. Grado (IT), June 20-22, 2002.

[RDF05] W. Ruml, M.B. Do, and M.P.J. Fromherz. Online Planning and Scheduling for High Speed Manufacturing. ICAPS05, 2005.

[RS05] S. Ratschan and Z. She. Safety verification of hybrid systems by constraint propagation based abstraction refinement. Hybrid Systems: Computation and Control (HSCC'05), LNCS 3114:573-589, 2005.

[RVW04] F. Rossi, K. B. Venable, T. Walsh. mCP nets: representing and reasoning with preferences of multiple agents, AAAI 2004, 2004.

[SICS] Swedish Institute of Computer Science. The SICStus Prolog Home Page. www.sics.se

[SJG96] V. A. Saraswat, R. Jagadeesan, and V. Gupta. Timed Default Concurrent Constraint Programming. Journal of Symbolic Computation, 22(5-6):475-520, 1996.

[SFV95] T. Schiex, H. Fargier and G. Verfaillie. Valued Constraint Satisfaction Problems: Hard and Easy Problems. Proc. of the Fourteenth International Joint Conference on Artificial Intelligence (IJCAI 95), pages 631-639. Morgan Kaufmann, 1995.

[T51] A. Tarski. A Decision Method for Elementary Algebra and Geometry. Univ. California, 1951.

[WWJ04] L. Wang, D. Wijesekera, and S. Jajodia. A Logic-based Framework for Attribute based Access Control. Proc. of 2nd ACM Workshop on Formal Methods in Security Engineering (FMSE 2004), 2004, 45-55

[Z78] L. A. Zadeh. Fuzzy Sets as a basis for the theory of possibility. Fuzzy sets and Systems, 13-28, 1978.
Parole Chiave
VINCOLI IN INTELLIGENZA ARTIFICIALE; PREFERENZE; PROGRAMMAZIONE CON VINCOLI; PROGRAMMAZIONE LOGICA CON VINCOLI; RISOLUTORI DI VINCOLI

Vincoli e preferenze come formalismo unificante per l'analisi di sistemi informatici e la soluzione di problemi reali

Università degli Studi di Padova
Abstract
La programmazione con vincoli e' un campo di ricerca multi-disciplinare in cui le competenze spaziano dalla Intelligenza Artificiale, alla Ricerca Operativa, ai Linguaggi di Programmazione, alle Basi di Dati, e le cui applicazioni sono presenti in molti discipline.

La programmazione con vincoli e' un paradigma di programmazione fondamentalmente diverso da molti altri, dato che richiede solo la modellazione di un problema in modo dichiarativo (specificando i suoi "vincoli") e poi la sua soluzione tramite una procedura generale che esplora lo spazio delle soluzioni e ne taglia parti inutili per mezzo di un uso attivo dei vincoli. Tipiche applicazioni della programmazione dei vincoli che hanno avuto molto successo sono i problemi di scheduling e di allocazione di risorse, i problemi di vehicle routing, gli orari, l'assegnamento delle frequenze. Nuovi campi applicativi che sono stati considerati negli ultimi anni sono
la bioinformatica, la configurazione online, la ricerca su web, e l'analisi di programmi e sistemi informatici.

La ricerca nel campo della programmazione con vincoli e' iniziata negli anni '70 nell'ambito dell'Intelligenza Artificiale e dal 1995 ha visto un aumento significativo dell'interesse sia teorico che pratico, con una conferenza internazionale annuale dedicata alla programmazione con vincoli, un'associazione internazionale, molti workshop e volumi,
una rivista internazionale, e cinque libri. L'Europa guida la >>>

Coordinatore Scientifico del Programma di Ricerca
Francesca ROSSI Università degli Studi di PADOVA
Obiettivo del Programma di Ricerca
L'obbiettivo di questo progetto e' studiare estensioni dei formalismi e delle tecniche esistenti per la programmazione con vincoli, con particolare riferimento ad applicazioni innovative sia a sistemi informatici (es. sicurezza, analisi di programmi) che a problemi reali (es. scheduling, bioinformatica). Utilizzeremo quindi i vincoli come formalismo unificante, e le applicazioni come spunto per le estensioni dei linguaggi e delle tecniche di risoluzione dei vincoli.

Unita' di ricerca

Per ottenere questo obbiettivo, abbiamo coinvolto alcuni tra i principali gruppi di lavoro in questo ambito di ricerca in Italia, in modo da poter sfruttare le competenze comuni per una facile comunicazione, ma anche le competenze complementari per una fruttuosa collaborazione che porti a nuovi risultati sia teorici che pratici. Tali gruppi sono presenti anche in un ambito di ricerca internazionale, e producono regolarmente risultati sia teorici che applicativi che vengono ben accolti dalla comunita' internazionale e hanno dato luogo a nuove linee di ricerca all'interno della programmazione con vincoli. In particolare:
-- l'unita' 1 (Padova), che coordina questo progetto, ha forti competenze nell'ambito dei vincoli soft e delle preferenze, e anche nell'applicazione di tecniche di vincoli a problemi di scheduling;
-- l'unita' 2 (Udine) ha esperienza nella definizione e sviluppo di nuovi linguaggi di programmazione logica con vincoli su >>>

Durata
24 mesi
Base di partenza scientifica nazionale o internazionale
La Programmazione con Vincoli [MS98,D03,A03] e' una metodologia di programmazione che permette di formalizzare il problema da risolvere in modo puramente dichiarativo con l'ausilio di formule logiche dette appunto vincoli. La fase di computazione e' tipicamente basata sulla ricerca di una o più soluzioni che soddisfino l'insieme di vincoli imposti. La Programmazione con Vincoli permette di tenere ben distinte la fase di formalizzazione da quella di ricerca delle soluzioni. Tuttavia anche questa seconda fase viene guidata dai vincoli che devono essere rispettati, al fine di ridurre sensibilmente lo spazio di ricerca.

Un risolutore di vincoli e' una procedura effettiva in grado di determinare la soddisfacibilità di vincoli e di trovare soluzioni che li soddisfino tutti, se esistono. Diversi risolutori sono stati proposti dagli anni '80 in poi, per vari domini di vincoli e con proprietà e tecniche implementative diverse. Molti di questi stati proposti nell'ambito della Programmazione Logica con Vincoli (CLP) [JM94], dove attualmente i sistemi più utilizzati sono SICStus Prolog [SICS] ed ECLiPSe [ECLI] che mettono a disposizione svariati domini di computazione e corrispondenti risolutori e sono stati impiegati con successo nella risoluzione di problemi di ottimizzazione o di ricerca di soluzioni ammissibili per problemi in domini complessi e con funzioni obiettivo arbitrarie.

L'utilizzo di vincoli su domini finiti permette di formulare problemi di >>>