-
A Unification Between Deep-Learning Vision, Compartmental Dynamical Thermodynamics, and Robotic Manipulation for a Circular Economy
Authors:
Federico Zocco,
Wassim M. Haddad,
Andrea Corti,
Monica Malvezzi
Abstract:
The shift from a linear to a circular economy has the potential to simultaneously reduce uncertainties of material supplies and waste generation. To date, the development of robotic and, more generally, autonomous systems have been rarely integrated into circular economy implementation strategies. In this review, we merge deep-learning vision, compartmental dynamical thermodynamics, and robotic ma…
▽ More
The shift from a linear to a circular economy has the potential to simultaneously reduce uncertainties of material supplies and waste generation. To date, the development of robotic and, more generally, autonomous systems have been rarely integrated into circular economy implementation strategies. In this review, we merge deep-learning vision, compartmental dynamical thermodynamics, and robotic manipulation into a theoretically-coherent physics-based research framework to lay the foundations of circular flow designs of materials, and hence, to speed-up the transition from linearity to circularity. Then, we discuss opportunities for robotics in circular economy.
△ Less
Submitted 23 May, 2024;
originally announced May 2024.
-
Model Checking for Rectangular Hybrid Systems: A Quantified Encoding Approach
Authors:
Luan V. Nguyen,
Wesam Haddad,
Taylor T. Johnson
Abstract:
Satisfiability Modulo Theories (SMT) solvers have been successfully applied to solve many problems in formal verification such as bounded model checking (BMC) for many classes of systems from integrated circuits to cyber-physical systems. Typically, BMC is performed by checking satisfiability of a possibly long, but quantifier-free formula. However, BMC problems can naturally be encoded as quantif…
▽ More
Satisfiability Modulo Theories (SMT) solvers have been successfully applied to solve many problems in formal verification such as bounded model checking (BMC) for many classes of systems from integrated circuits to cyber-physical systems. Typically, BMC is performed by checking satisfiability of a possibly long, but quantifier-free formula. However, BMC problems can naturally be encoded as quantified formulas over the number of BMC steps. In this approach, we then use decision procedures supporting quantifiers to check satisfiability of these quantified formulas. This approach has previously been applied to perform BMC using a Quantified Boolean Formula (QBF) encoding for purely discrete systems, and then discharges the QBF checks using QBF solvers. In this paper, we present a new quantified encoding of BMC for rectangular hybrid automata (RHA), which requires using more general logics due to the real (dense) time and real-valued state variables modeling continuous states. We have implemented a preliminary experimental prototype of the method using the HyST model transformation tool to generate the quantified BMC (QBMC) queries for the Z3 SMT solver. We describe experimental results on several timed and hybrid automata benchmarks, such as the Fischer and Lynch-Shavit mutual exclusion algorithms. We compare our approach to quantifier-free BMC approaches, such as those in the dReach tool that uses the dReal SMT solver, and the HyComp tool built on top of nuXmv that uses the MathSAT SMT solver. Based on our promising experimental results, QBMC may in the future be an effective and scalable analysis approach for RHA and other classes of hybrid automata as further improvements are made in quantifier handling in SMT solvers such as Z3.
△ Less
Submitted 14 July, 2022;
originally announced July 2022.
-
Spatial disconnection between stellar and dust emissions: the test of the Antennae Galaxies (Arp 244)
Authors:
L. -M. Seillé,
V. Buat,
W. Haddad,
A. Boselli,
M. Boquien,
L. Ciesla,
Y. Roehlly,
D. Burgarella
Abstract:
The detection with of the Atacama Large Millimeter Array (ALMA) of dust-rich high redshift galaxies whose cold dust emission is spatially disconnected from the ultraviolet emission bears a challenge for modelling their spectral energy distributions (SED) with codes based on an energy budget between the stellar and dust components. We test the validity of energy balance modelling on a nearby resolv…
▽ More
The detection with of the Atacama Large Millimeter Array (ALMA) of dust-rich high redshift galaxies whose cold dust emission is spatially disconnected from the ultraviolet emission bears a challenge for modelling their spectral energy distributions (SED) with codes based on an energy budget between the stellar and dust components. We test the validity of energy balance modelling on a nearby resolved galaxy with vastly different ultraviolet and infrared spatial distributions and infer what information can be reliably retrieved from the analysis of the full spectral energy distribution. We use 15 broadband images of the Antennae Galaxies ranging from far-ultraviolet to far-infrared and divide Arp 244 into 58 square ~1 kpc$^2$ regions. We fit the data with CIGALE to determine the star formation rate, stellar mass and dust attenuation of each region. We compare these quantities for the addition of the 58 regions to the ones obtained for Arp 244 as a whole and find that both estimates are consistent within one sigma. We present the spatial distribution of these physical parameters as well as the shape of the attenuation curve across the Antennae Galaxies . We also observe a flattening of the attenuation curves with increasing attenuation and dust surface density in agreement with the predictions of hydrodynamical simulations coupled with radiative transfer modelling.
△ Less
Submitted 16 July, 2022;
originally announced July 2022.
-
Thermodynamical Material Networks for Modeling, Planning, and Control of Circular Material Flows
Authors:
Federico Zocco,
Pantelis Sopasakis,
Beatrice Smyth,
Wassim M. Haddad
Abstract:
Waste production, carbon dioxide atmospheric accumulation, and dependence on finite natural resources are expressions of the unsustainability of the current industrial networks that supply fuels, energy, and manufacturing products. In particular, circular manufacturing supply chains and carbon control networks are urgently needed. To model and design these and, in general, any material networks, w…
▽ More
Waste production, carbon dioxide atmospheric accumulation, and dependence on finite natural resources are expressions of the unsustainability of the current industrial networks that supply fuels, energy, and manufacturing products. In particular, circular manufacturing supply chains and carbon control networks are urgently needed. To model and design these and, in general, any material networks, we propose to generalize the approach used for traditional networks such as water and thermal power systems by using compartmental dynamical thermodynamics and graph theory. The key idea is that the thermodynamic compartments and their connections can be added, removed or modified as needed to achieve a circular material flow. The design methodology is explained and its application is illustrated through examples. In addition, we provide a physics-based definition of circularity and, by implementing a nonlinear compartmental control, we strengthen the connection between "Industry 4.0" and "Sustainability". The paper source code is publicly available.
△ Less
Submitted 14 November, 2022; v1 submitted 20 November, 2021;
originally announced November 2021.
-
A Hand-Held Multimedia Translation and Interpretation System with Application to Diet Management
Authors:
Albert Parra,
Andrew W. Haddad,
Mireille Boutin,
Edward J. Delp
Abstract:
We propose a network independent, hand-held system to translate and disambiguate foreign restaurant menu items in real-time. The system is based on the use of a portable multimedia device, such as a smartphones or a PDA. An accurate and fast translation is obtained using a Machine Translation engine and a context-specific corpora to which we apply two pre-processing steps, called translation stand…
▽ More
We propose a network independent, hand-held system to translate and disambiguate foreign restaurant menu items in real-time. The system is based on the use of a portable multimedia device, such as a smartphones or a PDA. An accurate and fast translation is obtained using a Machine Translation engine and a context-specific corpora to which we apply two pre-processing steps, called translation standardization and $n$-gram consolidation. The phrase-table generated is orders of magnitude lighter than the ones commonly used in market applications, thus making translations computationally less expensive, and decreasing the battery usage. Translation ambiguities are mitigated using multimedia information including images of dishes and ingredients, along with ingredient lists. We implemented a prototype of our system on an iPod Touch Second Generation for English speakers traveling in Spain. Our tests indicate that our translation method yields higher accuracy than translation engines such as Google Translate, and does so almost instantaneously. The memory requirements of the application, including the database of images, are also well within the limits of the device. By combining it with a database of nutritional information, our proposed system can be used to help individuals who follow a medical diet maintain this diet while traveling.
△ Less
Submitted 16 July, 2018;
originally announced July 2018.
-
On the Global Dynamics of an Electroencephalographic Mean Field Model of the Neocortex
Authors:
Farshad Shirani,
Wassim M. Haddad,
Rafael de la Llave
Abstract:
This paper investigates the global dynamics of a mean field model of the electroencephalogram developed by Liley et al., 2002.
The model is presented as a system of coupled ordinary and partial differential equations with periodic boundary conditions.
Existence, uniqueness, and regularity of weak and strong solutions of the model are established in appropriate function spaces, and the associat…
▽ More
This paper investigates the global dynamics of a mean field model of the electroencephalogram developed by Liley et al., 2002.
The model is presented as a system of coupled ordinary and partial differential equations with periodic boundary conditions.
Existence, uniqueness, and regularity of weak and strong solutions of the model are established in appropriate function spaces, and the associated initial-boundary value problems are proved to be well-posed.
Sufficient conditions are developed for the phase spaces of the model to ensure nonnegativity of certain quantities in the model, as required by their biophysical interpretation.
It is shown that the semigroups of weak and strong solution operators possess bounded absorbing sets for the entire range of biophysical values of the parameters of the model.
Challenges towards establishing a global attractor for the model are discussed and it is shown that there exist parameter values for which the constructed semidynamical systems do not possess a compact global attractor due to the lack of the asymptotic compactness property.
Finally, using the theoretical results of the paper, instructive insights are provided into the complexity of the behavior of the model and computational analysis of the model.
△ Less
Submitted 4 May, 2017; v1 submitted 10 October, 2016;
originally announced October 2016.
-
Gait Assessment for Multiple Sclerosis Patients Using Microsoft Kinect
Authors:
Farnood Gholami,
Daria A. Trojan,
Jozsef Kovecses,
Wassim M. Haddad,
Behnood Gholami
Abstract:
Gait analysis of patients with neurological disorders, including multiple sclerosis (MS), is important for rehabilitation and treatment. The Mircrosoft Kinect sensor, which was developed for motion recognition in gaming applications, is an ideal candidate for an inexpensive system providing the capability for human gait analysis. In this research, we develop a framework to quantify the gait abnorm…
▽ More
Gait analysis of patients with neurological disorders, including multiple sclerosis (MS), is important for rehabilitation and treatment. The Mircrosoft Kinect sensor, which was developed for motion recognition in gaming applications, is an ideal candidate for an inexpensive system providing the capability for human gait analysis. In this research, we develop a framework to quantify the gait abnormality of MS patients using a Kinect for Windows camera. In addition to the previously introduced gait indices, a novel set of MS gait indices based on the concept of dynamic time war** is introduced. The newly introduced indices can characterize a patient's gait pattern as a whole and quantify a subject's gait distance from the healthy population. We will investigate the correlation of gait indices with the multiple sclerosis walking scale (MSWS) and the clinical ambulation score. This work establishes the feasibility of using the Kinect sensor for clinical gait assessment for MS patients.
△ Less
Submitted 10 August, 2015;
originally announced August 2015.
-
Segmentation of Facial Expressions Using Semi-Definite Programming and Generalized Principal Component Analysis
Authors:
Behnood Gholami,
Allen R. Tannenbaum,
Wassim M. Haddad
Abstract:
In this paper, we use semi-definite programming and generalized principal component analysis (GPCA) to distinguish between two or more different facial expressions. In the first step, semi-definite programming is used to reduce the dimension of the image data and "unfold" the manifold which the data points (corresponding to facial expressions) reside on. Next, GPCA is used to fit a series of sub…
▽ More
In this paper, we use semi-definite programming and generalized principal component analysis (GPCA) to distinguish between two or more different facial expressions. In the first step, semi-definite programming is used to reduce the dimension of the image data and "unfold" the manifold which the data points (corresponding to facial expressions) reside on. Next, GPCA is used to fit a series of subspaces to the data points and associate each data point with a subspace. Data points that belong to the same subspace are claimed to belong to the same facial expression category. An example is provided.
△ Less
Submitted 10 June, 2009; v1 submitted 9 June, 2009;
originally announced June 2009.
