Abstract

Abstract
In a restructured electricity sector, day-ahead markets can be modeled as a game where some players - the producers - submit their proposals. To analyze the companies' behavior we have used the concept of Nash equilibrium as a solution in these multi-agent interaction problems. In this paper, we present new and crucial adaptations of two well-known mechanisms, the adjustment process and the relaxation algorithm, in order to achieve the goal of computing Nash equilibria. The advantages of these approaches are highlighted and compared with those available in the literature.

Abstract
This chapter presents a general methodology for embodying simulation as part of a tree search procedure, as a technique for solving practical problems in combinatorial optimization. Target problems are either difficult to express as mixed integer optimization models, or have models which provide rather loose bounds; in both cases, traditional, exact methods typically fail. The idea then is to have tree search instantiating part of the variables in a systematic way, and for each particular instantiation-i.e., a node in the search tree-resort to a simulation for assigning values to the remaining variables; then, use the outcome of the simulation for evaluating that node in the tree. This method has been used with considerable success in gameplaying, but has received very limited attention as a tool for optimization. Nevertheless, it has great potential, either as a way for improving known heuristics or as an alternative to metaheuristics.We depart from repeated, randomized simulation based on problem-specific heuristics for applications in scheduling, logistics, and packing, and show how the systematic search in a tree improves the results that can be obtained. © Springer International Publishing Switzerland 2015.

Abstract
This article presents a semantics-based program verification framework for critical embedded real-time systems using the worst-case execution time (WCET) as the safety parameter. The verification algorithm is designed to run on devices with limited computational resources where efficient resource usage is a requirement For this purpose, the framework of abstract-carrying code (ACC) is extended with an additional verification mechanism for linear programming (LP) by applying the certifying properties of duality theory to check the optimality of WCET estimates. Further, the WCET verification approach preserves feasibility and scalability when applied to multicore architectural models. The certifying WCET algorithm is targeted to architectural models based on the ARM instruction set and is presented as a particular instantiation of a compositional data-flow framework supported on the theoretic foundations of denotational semantics and abstract interpretation. The data-flow framework has algebraic properties that provide algorithmic transformations to increase verification efficiency, mainly in terms of verification time. The WCET analysis/verification on multicore architectures applies the formalism of latency-rate (LR.) servers, and proves its correctness in the context of abstract interpretation, in order to ease WCET estimation of programs sharing resources.

Abstract
In this paper we describe a method for packing tubes and boxes in containers. Each container is divided into parts (holders) which are allocated to subsets of objects. The method consists of a recursive procedure which, based on a predefined order for dealing with tubes and boxes, determines the dimensions and position of each holder. Characteristics of the objects to pack and rules limiting their placement make this problem unique. The method devised provides timely and practical solutions.

Abstract