DSpace Collection:
http://hdl.handle.net/2117/3974
20141024T23:52:05Z

Narrow proofs may be maximally long
http://hdl.handle.net/2117/24406
Title: Narrow proofs may be maximally long
Authors: Atserias Peri, Albert; Lauria, Massimo; Nordström, Jakob
Abstract: We prove that there are 3CNF formulas over n variables that can be refuted in resolution in width w but require resolution proofs of size n¿(w). This shows that the simple counting argument that any formula refutable in width w must have a proof in size nO(¿) is essentially tight. Moreover, our lower bounds can be generalized to polynomial calculus resolution (PCR) and SheraliAdams, implying that the corresponding size upper bounds in terms of degree and rank are tight as well. Our results do not extend all the way to Lasserre, howeverthe formulas we study have Lasserre proofs of constant rank and size polynomial in both n and w.
20141017T11:02:37Z

A MAP approach for convex nonnegative matrix factorization in the diagnosis of brain tumors
http://hdl.handle.net/2117/24405
Title: A MAP approach for convex nonnegative matrix factorization in the diagnosis of brain tumors
Authors: Vilamala Muñoz, Albert; Belanche Muñoz, Luis Antonio; Vellido Alcacena, Alfredo
Abstract: Convex nonnegative matrix factorization is a blind signal separation technique that has previously demonstrated to be wellsuited for the task of human brain tumor diagnosis from magnetic resonance spectroscopy data. This is due to its ability to retrieve interpretable sources of mixed sign that highly correlate with tissue type prototypes. The current study provides a Bayesian formulation for such problem and derives a maximum a posteriori estimate based on a gradient descent algorithm specifically designed to deal with matrices with different sign restrictions. Its applicability to neurooncology diagnosis was experimentally assessed and the results were found to be comparable to those achieved by state of the art methods in tumor type discrimination and consistently better in source extraction.
20141017T09:54:45Z

Correctness of incremental model synchronization with triple graph grammars
http://hdl.handle.net/2117/24364
Title: Correctness of incremental model synchronization with triple graph grammars
Authors: Orejas Valdés, Fernando; Pino Blanco, Elvira
Abstract: In modeldriven software development, we may have several models describing the same system or artifact, by providing different views on it. In this case, we say that these models are consistently integrated. Triple Graph Grammars (TGGs), defined by Schürr, are a general and powerful tool to describe (bidirectional) model transformations. In this context, model synchronization is the operation that, given two consistent models and an update or modification of one of them, finds the corresponding update on the other model, so that consistency is restored. There are different approaches to describe this operation in terms of TGGs, but most of them have a computational cost that depends on the size of the given models. In general this may be very costly since these models may be quite large. To avoid this problem, Giese and Wagner have advocated for the need of incremental synchronization procedures, meaning that their cost should depend only on the size of the given update. In particular they proposed one such procedure. Unfortunately, the correctness of their approach is not studied and, anyhow, it could only be ensured under severe restrictions on the kind of TGGs considered. In the work presented, we study the problem from a different point of view. First, we discuss what it means for a procedure to be incremental, defining a correctness notion that we call incremental consistency. Moreover, we present a general incremental synchronization procedure and we show its correctness, completeness and incrementality.
20141014T11:38:12Z

Processoriented analysis for medical devices
http://hdl.handle.net/2117/24363
Title: Processoriented analysis for medical devices
Authors: Sfyrla, Vassiliki; Carmona Vargas, Josep; Henck, Pascal
Abstract: Medical Cyber Physical Systems are widely used in modern healthcare environments. Such systems are considered lifecritical due to the severity of consequences that faults may cause. Effective methods, techniques and tools for modeling and analyzing medical critical systems are of major importance for ensuring system reliability and patient safety. This work is looking at issues concerning different types of medical industry needs including safety analysis, testing, conformance checking, performance analysis and optimization. We explore the possibility of addressing these issues by exploiting information recorded in logs generated by medical devices during execution. Processoriented analysis of logs is known as process mining, a novel field that has gained considerable interest in several contexts in the last decade. Process mining techniques will be applied to an industrial use case provided by Fresenius, a manufacturer of medical devices, for analyzing process logs generated by an infusion pump.
20141014T09:28:19Z

The IntSat method for integer linear programming
http://hdl.handle.net/2117/24361
Title: The IntSat method for integer linear programming
Authors: Nieuwenhuis, Robert Lukas Mario
Abstract: ConflictDriven ClauseLearning (CDCL) SAT solvers can automatically solve very large realworld problems. To go beyond, and in particular in order to solve and optimize problems involving linear arithmetic constraints, here we introduce IntSat, a generalization of CDCL to Integer Linear Programming (ILP). Our simple 1400line C++ prototype IntSat implementation already shows some competitiveness with commercial solvers such as CPLEX or Gurobi. Here we describe this new IntSat ILP solving method, show how it can be implemented efficiently, and discuss a large list of possible enhancements and extensions.
20141014T07:43:08Z

Proving nontermination using maxSMT
http://hdl.handle.net/2117/24334
Title: Proving nontermination using maxSMT
Authors: Larraz Hurtado, Daniel; Nimkar, Kaustubh; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Rubio Gimeno, Alberto
Abstract: We show how MaxSMTbased invariant generation can be exploited for proving nontermination of programs. The construction of the proof of nontermination is guided by the generation of quasiinvariants  properties such that if they hold at a location during execution once, then they will continue to hold at that location from then onwards. The check that quasiinvariants can indeed be reached is then performed separately. Our technique considers strongly connected subgraphs of a program's control flow graph for analysis and thus produces more generic witnesses of nontermination than existing methods. Moreover, it can handle programs with unbounded nondeterminism and is more likely to converge than previous approaches.
20141010T06:28:12Z

Minimalmodelguided approaches to solving polynomial constraints and extensions
http://hdl.handle.net/2117/24333
Title: Minimalmodelguided approaches to solving polynomial constraints and extensions
Authors: Larraz Hurtado, Daniel; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Rubio Gimeno, Alberto
Abstract: In this paper we present new methods for deciding the satisfiability of formulas involving integer polynomial constraints. In previous work we proposed to solve SMT(NIA) problems by reducing them to SMT(LIA): nonlinear monomials are linearized by abstracting them with fresh variables and by performing case splitting on integer variables with finite domain. When variables do not have finite domains, artificial ones can be introduced by imposing a lower and an upper bound, and made iteratively larger until a solution is found (or the procedure times out). For the approach to be practical, unsatisfiable cores are used to guide which domains have to be relaxed (i.e., enlarged) from one iteration to the following one. However, it is not clear then how large they have to be made, which is critical. Here we propose to guide the domain relaxation step by analyzing minimal models produced by the SMT(LIA) solver. Namely, we consider two different cost functions: the number of violated artificial domain bounds, and the distance with respect to the artificial domains. We compare these approaches with other techniques on benchmarks coming from constraintbased program analysis and show the potential of the method. Finally, we describe how one of these minimalmodelguided techniques can be smoothly adapted to deal with the extension MaxSMT of SMT(NIA) and then applied to program termination proving.
20141010T06:16:02Z

An agentbased model studying the acquisition of a language system of logical constructions
http://hdl.handle.net/2117/24301
Title: An agentbased model studying the acquisition of a language system of logical constructions
Authors: Sierra Santibáñez, Josefina
Abstract: This paper presents an agentbased model that studies the emergence and evolution of a language system of logical constructions,
i.e. a vocabulary and a set of grammatical constructions that allows the expression of logical combinations of categories. The model assumes the agents have a common vocabulary for basic categories, the ability to construct logical combinations of categories using Boolean functions, and some general purpose cognitive capacities for invention, adoption, induction and adaptation. But it does not assume the agents have a vocabulary for Boolean functions nor grammatical constructions for expressing such logical combinations of categories through language. The results of the experiments we have performed show that a language system of logical constructions emerges as a result of a process of selforganisation of the individual agents’ interactions when these agents adapt their preferences for vocabulary and grammatical constructions to those they observe are used more often by the rest of the population, and that such a language system is transmitted from one generation to the next.
20141008T09:01:59Z

A multiagent experiment on the acquisition of a language system of logical constructions
http://hdl.handle.net/2117/24299
Title: A multiagent experiment on the acquisition of a language system of logical constructions
Authors: Sierra Santibáñez, Josefina
Abstract: This paper analyses an experiment which studies the acquisition of the linguistic competence required to communicate logical combinations of categories from the wisdom of the crowds perspective. The acquisition of such competence encompasses both the construction of a set of logical categories by each individual agent and of a shared language by the population. The processes of conceptualisation and language acquisition in each individual agent are based on general purpose cognitive capacities such as discrimination, invention, adoption and induction. The construction of a shared language by the population is achieved using a particular type of linguistic interaction, known as the evaluation game, which gives rise to a shared language system of logical constructions as a result of a process of selforganisation of the individual agents’ interactions, when these agents adapt their languages to the expressions they observe are used more often by other agents.
20141008T08:30:14Z

On the average performance of fixed partial match queries in random relaxed Kd trees
http://hdl.handle.net/2117/24268
Title: On the average performance of fixed partial match queries in random relaxed Kd trees
Authors: Duch Brown, Amalia; Lau LaynesLozada, Gustavo Salvador; Martínez Parra, Conrado
Abstract: We obtain an explicit formula for the expected cost of a fixed partial match query in a random relaxed Kd tree, that is, the expected cost for a query of the form q = (q0 , q1 , . . . , qK1 ) with 0 < s < K specified coordinates with values z0 , . . . , zs1 ¿ (0, 1). This is a generalization of previous results in the literature for s = 1. Qualitatively similar results hold for standard Kd trees and we conjecture that this also holds for other multidimensional tree structures such as quadtrees and Kd tries.
20141006T09:14:06Z

Estimation of machine settings for spinning of yarns : new algorithms for comparing complex structures
http://hdl.handle.net/2117/24256
Title: Estimation of machine settings for spinning of yarns : new algorithms for comparing complex structures
Authors: Sevilla Villanueva, Beatriz; Sánchez Marrè, Miquel; Fischer, Thomas V.
Abstract: The textile industry in Europe is facing a new challenge in order to stay competitive into the textile market. They need to be flexible, cost efficient and produce with high quality. The setting of the machinery parameters is therefore an important aspect that combines implicit knowledge of workers and engineers with explicit knowledge. This makes it an ideal domain for CBR. It is used for an automatic parameter setting but the data cannot be reduced to a flat representation, as yarns and fabrics are multicomponent artefacts. Therefore we propose a combination of 4 algorithms to evaluate the similarity of the yarns. The application was successfully applied for spinning and it can be applied in the following steps of the textile processes like weaving
20141005T07:33:21Z

Automatic evaluation of reductions between NPcomplete problems
http://hdl.handle.net/2117/24254
Title: Automatic evaluation of reductions between NPcomplete problems
Authors: Creus López, Carles; Fernández Durán, Pau; Godoy Balil, Guillem
Abstract: We implement an online judge for evaluating correctness of reductions between NPcomplete problems. The site has a list of exercises asking for a reduction between two given problems. Internally, the reduction is evaluated by means of a set of tests. Each test consists of an input of the first problem and gives rise to an input of the second problem through the reduction. The correctness of the reduction, that is, the preservation of the answer between both problems, is checked by applying additional reductions to SAT and using a stateoftheart SAT solver. In order to represent the reductions, we have defined a new programming language called REDNP. On one side, REDNP has specific features for describing typical concepts that frequently appear in reductions, like graphs and clauses. On the other side, we impose severe limitations to REDNP in order to avoid malicious submissions, like the ones with an embedded SAT solver.
20141005T06:34:30Z

Automatic evaluation of contextfree grammars (system description)
http://hdl.handle.net/2117/24226
Title: Automatic evaluation of contextfree grammars (system description)
Authors: Creus López, Carles; Godoy Balil, Guillem
Abstract: We implement an online judge for contextfree grammars. Our system contains a list of problems describing formal languages, and asking for grammars generating them. A submitted proposal grammar receives a verdict of acceptance or rejection depending on whether the judge determines that it is equivalent to the reference solution grammar provided by the problem setter. Since equivalence of contextfree grammars is an undecidable problem, we consider a maximum length l and only test equivalence of the generated languages up to words of length l. This length restriction is very often sufficient for the wellmeant submissions. Since this restricted problem is still NPcomplete, we design and implement methods based on hashing, SAT, and automata that perform well in practice. © 2014 Springer International Publishing Switzerland.
20141003T07:01:26Z

Tree automata with height constraints between brothers
http://hdl.handle.net/2117/24225
Title: Tree automata with height constraints between brothers
Authors: Creus López, Carles; Godoy Balil, Guillem
Abstract: We define the tree automata with height constraints between brothers (TACBB H ). Constraints of equalities and inequalities between heights of siblings that restrict the applicability of the rules are allowed in TACBB H. These constraints allow to express natural tree languages like complete or balanced (like AVL) trees. We prove decidability of emptiness and finiteness for TACBB H, and also for a more general class that additionally allows to combine equality and disequality constraints between brothers. © 2014 Springer International Publishing Switzerland.
20141003T06:29:03Z

Metastability in betterthanworstcase designs
http://hdl.handle.net/2117/24174
Title: Metastability in betterthanworstcase designs
Authors: Beer, Salomon; Cannizzaro, Marco; Cortadella Fortuny, Jordi; Ginosar, Ran; Lavagno, Luciano
Abstract: BetterThanWorstCaseDesigns use timing speculation to run with a cycle period faster than the one required for worstcase conditions. This speculation may produce timing violations and metastability that result in failures and nondeterministic timing behavior. The effects of these phenomena are not always well understood by designers and researchers in this area. This paper analyzes the impact of timing speculation and the reasons why it is difficult to adopt this paradigm in industrial designs.
20140926T10:14:18Z