Deciding Kleene Algebra Terms Equivalence in Coq

This paper presents a mechanically verified implementation of an algorithm for deciding the equivalence of Kleene algebra terms within the Coq proof assistant. The algorithm decides equivalence of two given regular expressions through an iterated process of testing the equivalence of their partial derivatives and does not require the construction of the corresponding automata. Recent theoretical and experimental research provides evidence that this method is, on average, more efficient than the classical methods based on automata. We present some performance tests, comparisons with similar approaches, and also introduce a generalization of the algorithm to decide the equivalence of terms of Kleene algebra with tests. The motivation for the work presented in this paper is that of using the libraries developed as trusted frameworks for carrying out certified program verification.

Application mapping in NoC-Based many-cores

Many-core platforms based on Network-on-Chip (NoC [Benini and De Micheli 2002]) present an emerging technology in the real-time embedded domain. Although the idea to group the applications previously executed on separated single-core devices, and accommodate them on an individual many-core chip offers various options for power savings, cost reductions and contributes to the overall system flexibility, its implementation is a non-trivial task. In this paper we address the issue of application mapping onto a NoCbased many-core platform when considering fundamentals and trends of current many-core operating systems, specifically, we elaborate on a limited migrative application model encompassing a message-passing paradigm as a communication primitive. As the main contribution, we formulate the problem of real-time application mapping, and propose a three-stage process to efficiently solve it. Through analysis it is assured that derived solutions guarantee the fulfilment of posed time constraints regarding worst-case communication latencies, and at the same time provide an environment to perform load balancing for e.g. thermal, energy, fault tolerance or performance reasons.We also propose several constraints regarding the topological structure of the application mapping, as well as the inter- and intra-application communication patterns, which efficiently solve the issues of pessimism and/or intractability when performing the analysis.

Projeto topológico de uma rede rodoviária

Mestrado em Engenharia Informática - Área de Especialização em Sistemas Gráficos e Multimédia

Coordinated transportation of a large object by a team of three robots

Dynamical systems theory in this work is used as a theoretical language and tool to design a distributed control architecture for a team of three robots that must transport a large object and simultaneously avoid collisions with either static or dynamic obstacles. The robots have no prior knowledge of the environment. The dynamics of behavior is defined over a state space of behavior variables, heading direction and path velocity. Task constraints are modeled as attractors (i.e. asymptotic stable states) of the behavioral dynamics. For each robot, these attractors are combined into a vector field that governs the behavior. By design the parameters are tuned so that the behavioral variables are always very close to the corresponding attractors. Thus the behavior of each robot is controlled by a time series of asymptotical stable states. Computer simulations support the validity of the dynamical model architecture.

Coordinated transportation of a large object by a team of two robots

In this paper dynamical systems theory is used as a theoretical language and tool to design a distributed control architecture for a team of two robots that must transport a large object and simultaneously avoid collisions with obstacles (either static or dynamic). This work extends the previous work with two robots (see [1] and [5]). However here we demonstrate that it’s possible to simplify the architecture presented in [1] and [5] and reach an equally stable global behavior. The robots have no prior knowledge of the environment. The dynamics of behavior is defined over a state space of behavior variables, heading direction and path velocity. Task constrains are modeled as attractors (i.e. asymptotic stable states) of a behavioral dynamics. For each robot, these attractors are combined into a vector field that governs the behavior. By design the parameters are tuned so that the behavioral variables are always very close to the corresponding attractors. Thus the behavior of each robot is controlled by a time series of asymptotic stable states. Computer simulations support the validity of the dynamical model architecture.

Using attractor dynamics to generate decentralized motion control of two mobile robots transporting a long object in coordination

Dynamical systems theory is used here as a theoretical language and tool to design a distributed control architecture for a team of two mobile robots that must transport a long object and simultaneously avoid obstacles. In this approach the level of modeling is at the level of behaviors. A “dynamics” of behavior is defined over a state space of behavioral variables (heading direction and path velocity). The environment is also modeled in these terms by representing task constraints as attractors (i.e. asymptotically stable states) or reppelers (i.e. unstable states) of behavioral dynamics. For each robot attractors and repellers are combined into a vector field that governs the behavior. The resulting dynamical systems that generate the behavior of the robots may be nonlinear. By design the systems are tuned so that the behavioral variables are always very close to one attractor. Thus the behavior of each robot is controled by a time series of asymptotically stable states. Computer simulations support the validity of our dynamic model architectures.

Seasonal patterns of polycyclic aromatic hydrocarbons in digestive gland and arm of octopus (Octopus vulgaris) from the Northwest Atlantic

Among organic pollutants existing in coastal areas, polycyclic aromatic hydrocarbons (PAHs) are of great concern due to their ubiquity and carcinogenic potential. The aim of this study was to evaluate the seasonal patterns of PAHs in the digestive gland and arm of the common octopus (Octopus vulgaris) from the Northwest Atlantic Portuguese coast. In the different seasons, 18 PAHs were determined and the detoxification capacity of the species was evaluated. Ethoxyresorufin O-deethylase (EROD) and ethoxycoumarin O-deethylase (ECOD) activities were measured to assess phase I biotransformation capacity. Individual PAH ratios were used for major source (pyrolytic/petrogenic) analysis. Risks for human consumption were determined by the total toxicity equivalence approach. Generally, low levels of PAHs were detected in the digestive gland and in the arm of octopus, with a predominance of low molecular over high molecular weight compounds. PAHs exhibited seasonality in the concentrations detected and in their main emission sources. In the digestive gland, the highest total PAH levels were observed in autumn possibly related to fat availability in the ecosystem and food intake. The lack of PAH elimination observed in the digestive gland after captivity could be possibly associated to a low biotransformation capacity, consistent with the negligible/undetected levels of EROD and ECOD activity in the different seasons. The emission sources of PAHs found in the digestive gland varied from a petrogenic profile observed in winter to a pyrolytic pattern in spring. In the arm, the highest PAH contents were observed in June; nevertheless, levels were always below the regulatory limits established for food consumption. The carcinogenic potential calculated for all the sampling periods in the arm were markedly lower than the ones found in various aquatic species from different marine environments. The results presented in this study give relevant baseline data for environmental monitoring of organic pollution in coastal areas.

Definition of Distribution Network Tariffs Considering Distribution Generation and Demand Response

The use of distribution networks in the current scenario of high penetration of Distributed Generation (DG) is a problem of great importance. In the competitive environment of electricity markets and smart grids, Demand Response (DR) is also gaining notable impact with several benefits for the whole system. The work presented in this paper comprises a methodology able to define the cost allocation in distribution networks considering large integration of DG and DR resources. The proposed methodology is divided into three phases and it is based on an AC Optimal Power Flow (OPF) including the determination of topological distribution factors, and consequent application of the MW-mile method. The application of the proposed tariffs definition methodology is illustrated in a distribution network with 33 buses, 66 DG units, and 32 consumers with DR capacity.

Explosion of smoothness from a point to everywhere for conjugacies between Markov families

For uniformly asymptotically affine (uaa) Markov maps on train tracks, we prove the following type of rigidity result: if a topological conjugacy between them is (uaa) at a point in the train track then the conjugacy is (uaa) everywhere. In particular, our methods apply to the case in which the domains of the Markov maps are Canter sets. We also present similar statements for (uaa:) and C-r Markov families. These results generalize the similar ones of Sullivan and de Faria for C-r expanding circle maps with r > 1 and have useful applications to hyperbolic dynamics on surfaces and laminations.

Explosion of smoothness from a point to everywhere for conjugacies between diffeomorphisms on surfaces

For diffeomorphisms on surfaces with basic sets, we show the following type of rigidity result: if a topological conjugacy between them is differentiable at a point in the basic set then the conjugacy has a smooth extension to the surface. These results generalize the similar ones of D. Sullivan, E. de Faria and ours for one-dimensional expanding dynamics.

Cost allocation model for distribution networks considering high penetration of distributed energy resources

The high penetration of distributed energy resources (DER) in distribution networks and the competitive environment of electricity markets impose the use of new approaches in several domains. The network cost allocation, traditionally used in transmission networks, should be adapted and used in the distribution networks considering the specifications of the connected resources. The main goal is to develop a fairer methodology trying to distribute the distribution network use costs to all players which are using the network in each period. In this paper, a model considering different type of costs (fixed, losses, and congestion costs) is proposed comprising the use of a large set of DER, namely distributed generation (DG), demand response (DR) of direct load control type, energy storage systems (ESS), and electric vehicles with capability of discharging energy to the network, which is known as vehicle-to-grid (V2G). The proposed model includes three distinct phases of operation. The first phase of the model consists in an economic dispatch based on an AC optimal power flow (AC-OPF); in the second phase Kirschen's and Bialek's tracing algorithms are used and compared to evaluate the impact of each resource in the network. Finally, the MW-mile method is used in the third phase of the proposed model. A distribution network of 33 buses with large penetration of DER is used to illustrate the application of the proposed model.