Catálogo de publicaciones - libros

Model Checking is a well-known and fully automatic technique for checking software properties, usually given as temporal logic formulae on the program variables. Most model checkers found in the literature use exact deterministic algorithms to check the properties. These algorithms usually require huge amounts of computational resources if the checked model is large. We propose here the use of Ant Colony Optimization (ACO) to refute safety properties in concurrent systems. ACO algorithms are stochastic techniques belonging to the class of metaheuristic algorithms and inspired by the foraging behaviour of real ants. The results state that ACO algorithms find optimal or near optimal error trails in faulty concurrent systems with a reduced amount of resources, outperforming algorithms that are the state-of-the-art in model checking. This fact makes them suitable for checking safety properties in large concurrent systems, in which traditional techniques fail to find errors because of the model size.

We discuss how to combine 01X-logic and quantified boolean formulas (QBF) within a homogeneous SAT/QBF-framework in the context of bounded model checking of blackbox designs. The proposed combination allows a flexible handling of blackboxes w.r.t. computational resources. Preliminary results show the scalability of the approach.

SAT-based bounded model checking has been introduced as a complementary technique to BDD-based symbolic model checking in recent years and a lot of successful work has been done with this approach. The success is mostly due to the efficiency of error-detection. Verification of valid properties depends on a completeness threshold that could be too large to be practical. We discuss an approach to checking valid ACTL (the universal fragment of CTL) properties similar to bounded model checking of ACTL. Bounded model checking of ATCL has been considered in [8]. Given a model and an ACTL formula , a series of -models of are constructed for  = 0,1,2,..., and the process for checking proceeds as follows: start with the 0-model, if the model does not satisfy the negation of , use 1-model and so forth, until the negation of is satisfied or until a bound of is reached. A general bound for is the number of states of . Trying all -models up to the bound in order to obtain a conclusion is obviously not desirable. For attacking this problem, we propose an approach to (partly) avoid the use of such a bound.

Combiner construction is an important problem in the design of random generators for applications in stream ciphering. Most constructions use the concept of static combiners based on boolean functions. In this paper we propose the construction of a dynamic combiner which is based on a cellular array of finite state machines which realize a switching network for a XOR combiner with variable length.

We show how an arbitrary finite number of CA with different local rules can be simulated by CA using by just changing the (shape of the) neighborhood. In that way one can even achieve universality.

In this paper a study about the modelling, simulation and implementation on reconfigurable hardware of the Conway’s Game of Life is shown. The Game of Life is a very popular case of cellular automata. The purpose of this study was to know the capability to model cellular automata by means of the high level hardware description language Handel-C, and to determine a first approximation to the hardware performance of the algorithm by means of the simulation of the implementation on reconfigurable FPGA devices. We can say, thanks to the found results, that the employed modelling technique allows us to prototype easily in short time this kind of algorithms, and the obtained simulation timing results are better than the found in a software version, up to a determined high number of iterations of the game.

We are presenting results of the creature’s exploration problem with several creatures. The task of the creatures is to visit all empty cells in an environment with obstacles in shortest time and with a maximum of efficiency. The cells are arranged in a regular 2D grid and the underlying processing model is a Cellular Automaton (CA). We have investigated the question how many creatures and which algorithm should be used in order to fulfill the task most efficiently with lowest cost. We use a set of 10 different behaviors (algorithms) for the creature which have proved to be very efficient in the case where only one creature explores the environment. These algorithms were found by exhaustive search and evaluation by the aid of hardware (FPGA) implementation. Different environments and a varying number (1 to 64) of creatures were used in simulations in order to evaluate the cooperative work and efficiency. It turned out that for each environment a certain number of creatures and a certain algorithm is cost optimal in terms of work units. The total amount of work using one creature with the best algorithm X is many cases higher than the work using creature with an adequate algorithm Y. Using several creatures, positive conflicts arise which may help to solve the problem more efficiently.

The firing squad synchronization problem on cellular automata has been studied extensively for more than forty years, and a rich variety of synchronization algorithms have been proposed so far. In the present paper, we propose a new optimum-time algorithm for synchronizing two-dimensional cellular automata. The algorithm can synchronize any rectangular array of size × in optimum  +  + (, ) − 3 steps.

Estimation of motion has many applications in fluid analysis. Lots of work has been carried out using Particle Image Velocimetry to design experiments which capture and measure the flow motion using 2D images. Recent technological advances allow capturing 3D PIV image sequences of moving particles. In this context, we propose a 3D motion estimation technique based on the combination of an iterative cross-correlation technique and a variational (energy-based) technique. The performance of the proposed technique is measured and illustrated using numerical simulations.

In this paper we propose a novel approach for the control of helicopters, using a flight dynamics model of the aircraft to develop reliable controllers by means of classical procedures, evolutionary either reinforcement learning techniques. Here we are presenting the method that we use to estimate the aircraft position, including the low level image processing, the hardware configuration which allows us to register the commands generated by an expert pilot using a conventional radio control (RC) transmitter, and how both variables are related by an artificial neural network (ANN).