Loading...
Loading...

Go to the content (press return)

A declarative approach to model, analyse and solve problems

Total activity: 1
Type of activity
Competitive project
Acronym
DAMAS
Funding entity
MIN DE ECONOMIA Y COMPETITIVIDAD
Funding entity code
TIN2013-45732-C4-3-P
Amount
35.592,15 €
Start date
2014-01-01
End date
2016-06-30
Abstract
Hard decision and optimization problems are present in many applications of computational tools. Some challenging
questions are: how do we schedule a professional sports league, whether a cryptographic protocol is safe, whether there
is some input data that will cause a program to hang or produce wrong output, which is the most convenient time slot for
a video conference, how can a flexible admission control for safe overbooking be defined for cloud computing, or how a
flexible text cataloging and information retrieval can be defined for the (semantic) web.
A declarative approach to solve such problems consists in modelling the problem in some logical framework and then
applying powerful logic-based techniques to analyse and/or solve the resulting model. In this setting, problems can often
be formulated using mathematical formulas or other logic-based languages. Once the problem is expressed in the
corresponding language we can use existing general techniques or develop novel ones to solve it. When this approach
is applied to our specific problems, we might need to use some of their particularities in order to improve its performance.
However, thanks to the initial abstraction from particular problems to general problems expressed in a given language,
this "declarative approach" makes the development of tools to solve hard real problems significantly easier and faster.
As logical frameworks we will mainly use (extensions of) propositional and first-order logic. In particular, we will consider:
SAT (satisfaction of propositional formulas), SAT modulo theories (SMT, where propositions are replaced by atoms in
the given theory), Constraint Programming (CP, where clauses are replaced by predicates over a pre-defined language),
Fuzzy Logic (FL, where clauses have some uncertainty), Rewrite Logic (RWL, with modelling and programming
advanced capabilities), Logic Programming (LP), and Fuzzy Logic Programming (FLP). In this project we will focus on
the combination and extension of these successful formal languages to get the necessary expressiveness for our
practical applications.
Guided by applications for scheduling and planning, for security, for agents, for machine learning, for concurrent and
sequential program analysis, for bio-informatics or for XML manipulation, we will develop efficient algorithms and tools to
solve problems described in the previous logical frameworks.
As precise applications we consider: (a) sports scheduling as done with Hypercube and KNVB, the Netherlands, (b)
program analysis in collaboration with Microsoft Research at Cambridge, (c) evaluation of transcript sequences in
collaboration with the Centre for Genomic Regulation (CRG) in Barcelona, (d) security in collaboration with the University
of Illinois at Urbana-Champaign and the Naval Research Laboratory at Washington, (e) new features in the Maude
language with the University of Illinois at Urbana-Champaign and SRI International in California, (f) knowledge discovering and flexible manipulation of data retrieved from the web in collaboration with the University of Almería, and
(g) fuzzy scheduling for resource usage within cloud data centers with the Umeå University.
This is therefore a project that covers all the way in the development and application of computer technologies from the
basic theory and techniques to industrial and social impact problems.
Keywords
análisis y verificación de programas, constraint solving, formula satisfiability, logics, lógicas, program analysis and verification, resolución de restricciones, satisfacibilidad de fórmulas
Scope
Adm. Estat
Plan
Plan Estatal de Investigación Científica y Técnica y de Innovación 2013-2016
Resoluton year
2014
Funcding program
Programa Estatal de Fomento de la Investigación Científica y Técnica de Excelencia
Funding subprogram
Subprograma Estatal de Generación de Conocimiento
Funding call
Excelencia: Proyectos I+D
Grant institution
Gobierno De España. Ministerio De Economía Y Competitividad, Mineco

Participants

Scientific and technological production

1 to 1 of 1 results