Person:
Rodríguez Laguna, Ismael

First Name

Ismael

Last Name

Rodríguez Laguna

Affiliation

Universidad Complutense de Madrid

Faculty / Institute

Informática

Department

Sistemas Informáticos y Computación

Area

Lenguajes y Sistemas Informáticos

Identifiers

Full item page

Search Results

Now showing 1 - 10 of 22

A formal framework to test soft and hard deadlines in timed systems
(Wiley-Blackwell, 2012-12) García Merayo, Mercedes; Núñez García, Manuel; Rodríguez Laguna, Ismael
This paper introduces a formal framework to specify and test systems presenting both soft and hard deadlines. While hard deadlines must always be met on time, soft deadlines can be sometimes met in a different time, usually greater, from the specified one. It is this characteristic (to formally definetextitsometimes) that produces several reasonable alternatives to define appropriate implementation relations, that is, relations to decide whether an implementation is correct with respect to a specification. In addition to introducing these relations, the paper also presents a formal testing framework to test implementations and provides an algorithm to derive sound and complete test suites with respect to the implementation relations previously defined. That is, an implementation conforms to a specification if and only if the implementation successfully passes all the tests belonging to the suite derived from the specification.
A logic for assessing sets of heterogeneous testing hypotheses
(Springer Verlag, 2006) García Merayo, Mercedes; Rodríguez Laguna, Ismael; Núñez García, Manuel
To ensure the conformance of an implementation under test (IUT) with respect to a specification requires, in general, the application of an infinite number of tests. In order to use finite test suites, most testing methodologies add some feasible hypotheses about the behavior of the IUT. Since these methodologies are designed for considering a fix set of hypotheses, they usually do not have the capability of dealing with other scenarios where the set of assumed hypotheses varies. We propose a logic to infer whether a set of observations (i.e., results of test applications) allows to claim that the IUT conforms to the specification if a specific set of hypotheses (taken from a repertory) is assumed.
On the Hardness of Lying under Egalitarian Social Welfare
(MDPI, 2021-07-07) Carrero Aranda, Jonathan; Rodríguez Laguna, Ismael; Rubio Diez, Fernando
When it comes to distributing resources among different agents, there are different objectives that can be maximized. In the case of egalitarian social welfare, the goal is to maximize the utility of the least satisfied agent. Unfortunately, this goal can lead to strategic behaviors on the part of the agents: if they lie about their utility functions, then the dealer might grant them more goods than they would be entitled to. In this work, we study the computational complexity of obtaining the optimal lie in this context. We show that although it is extremely easy to obtain the optimal lie when we do not impose any restrictions on the lies used, the problem becomes Σ P 2 -complete by imposing simple limits on the usable lies. Thus, we prove that we can easily make it hard to lie in the context of egalitarian social welfare.
Parallelizing Particle Swarm Optimization in a Functional Programming Environment
(MDPI, 2014-10-23) Rabanal Basalo, Pablo Manuel; Rodríguez Laguna, Ismael; Rubio Díez, Fernando
Many bioinspired methods are based on using several simple entities which search for a reasonable solution (somehow) independently. This is the case of Particle Swarm Optimization (PSO), where many simple particles search for the optimum solution by using both their local information and the information of the best solution found so far by any of the other particles. Particles are partially independent, and we can take advantage of this fact to parallelize PSO programs. Unfortunately, providing good parallel implementations for each specific PSO program can be tricky and time-consuming for the programmer. In this paper we introduce several parallel functional skeletons which, given a sequential PSO implementation, automatically provide the corresponding parallel implementations of it. We use these skeletons and report some experimental results. We observe that, despite the low effort required by programmers to use these skeletons, empirical results show that skeletons reach reasonable speedups.
THOTL: A timed extension of HOTL
(SPRINGER-VERLAG BERLIN, 2008) García Merayo, Mercedes; Núñez García, Manuel; Rodríguez Laguna, Ismael
THOTL represents a conservative extension of HOTL (Hypotheses and Observations Testing Logic) to deal with systems where time plays a fundamental role. We adapt some of the HOTL rules to cope with the new framework. In addition, we introduce several specific hypotheses and rules to appropriately express time assumptions. We provide a correctness result of THOTL with respect to a general notion of timed conformance.
Herramienta para escoger sistemáticamente combinaciones de ejercicios con mayor capacidad formadora y/o evaluadora
(2017-06-30) Rodríguez Laguna, Ismael; de la Encina Vara, Alberto; Garbayo Moreno, Martín Manuel; Hidalgo Herrero, Mercedes; López Barquilla, Natalia; Rabanal Basalo, Pablo Manuel; Rubio Diez, Fernando
Formal testing of systems presenting soft and hard deadlines
(SPRINGER-VERLAG BERLIN, 2007) García Merayo, Mercedes; Núñez García, Manuel; Rodríguez Laguna, Ismael; Arbab, F; Sirjani, M
We present a formal framework to specify and test systems presenting both soft and hard deadlines. While hard deadlines must be always met on time, soft deadlines can be sometimes met in a different time, usually higher, from the specified one. It is this characteristic (to formally define sometimes) what produces several reasonable alternatives to define appropriate implementation relations, that is, relations to decide wether an implementation is correct with respect to a specification. In addition to introduce these relations, we define a testing framework to test implementations.
Extending EFSMs to specify and test timed systems with action duration and time-outs
(Institute of Electrical and Electronics Engineers, 2008-06) García Merayo, Mercedes; Núñez García, Manuel; Rodríguez Laguna, Ismael
In this paper, we introduce a timed extension of the extended finite state machines model. On one hand, we consider that (output) actions take time to be performed. This time may depend on several factors, such as the value of variables. On the other hand, our formalism allows us to specify time-outs. In addition to presenting our language, we develop a testing theory. First, we define 10 timed conformance relations and relate them. Second, we introduce a notion of timed test and define how to apply tests to implementations. Finally, we give an algorithm to derive sound and complete test suites with respect to the implementation relations presented in the paper. This paper represents an extended and improved version of
Towards Applying River Formation Dynamics in Continuous Optimization Problems
(Springer Verlag, 2019) Rabanal Basalo, Pablo Manuel; Rodríguez Laguna, Ismael; Rubio Díez, Fernando
River Formation Dynamics (RFD) is a metaheuristic that has been successfully used by different research groups to deal with a wide variety of discrete combinatorial optimization problems. However, no attempt has been done to adapt it to continuous optimization domains. In this paper we propose a first approach to obtain such objective, and we evaluate its usefulness by comparing RFD results against those obtained by other more mature metaheuristics for continuous domains. In particular, we compare with the results obtained by Particle Swarm Optimization, Artificial Bee Colony, Firefly Algorithm, and Social Spider Optimization.
Generalization and completeness of stochastic local search algorithms
(Elsevier, 2021-09-15) Loscos Barroso, Daniel; Martí Oliet, Narciso; Rodríguez Laguna, Ismael
We generalize Stochastic Local Search (SLS) heuristics into a unique formal model. This model has two key components: a common structure designed to be as large as possible and a parametric structure intended to be as small as possible. Each heuristic is obtained by instantiating the parametric part in a different way. Particular instances for Genetic Algorithms (GA), Ant Colony Optimization (ACO), and Particle Swarm Optimization (PSO) are presented. Then, we use our model to prove the Turing-completeness of SLS algorithms in general. The proof uses our framework to construct a GA able to simulate any Turing machine. This Turing-completeness implies that determining any non-trivial property concerning the relationship between the inputs and the computed outputs is undecidable for GA and, by extension, for the general set of SLS methods (although not necessarily for each particular method). Similar proofs are more informally presented for PSO and ACO.