skip to main content

Title: Mining Shape Expressions from Positive Examples
Shape expressions (SEs) is a novel specification language that was recently introduced to express behavioral patterns over real-valued signals observed during the execution of cyber-physical systems. An SE is a regular expression composed of arbitrary parameterized shapes, such as lines, exponential curves, and sinusoids as atomic symbols with symbolic constraints on the shape parameters. SEs enable a natural and intuitive specification of complex temporal patterns over possibly noisy data. In this article, we propose a novel method for mining a broad and interesting fragment of SEs from time-series data using a combination of techniques from linear regression, unsupervised clustering, and learning finite automata from positive examples. The learned SE for a given dataset provides an explainable and intuitive model of the observed system behavior. We demonstrate the applicability of our approach on two case studies from different application domains and experimentally evaluate the implemented specification mining procedure.
; ; ; ; ;
Award ID(s):
Publication Date:
Journal Name:
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
Page Range or eLocation-ID:
1 to 1
Sponsoring Org:
National Science Foundation
More Like this
  1. All-solid-state batteries (ASSBs) have garnered increasing attention due to the enhanced safety, featuring nonflammable solid electrolytes as well as the potential to achieve high energy density. 1 The advancement of the ASSBs is expected to provide, arguably, the most straightforward path towards practical, high-energy, and rechargeable batteries based on metallic anodes. 1 However, the sluggish ion transmission at the cathode-electrolyte (solid/solid) interface would result in the high resistant at the contact and limit the practical implementation of these all solid-state materials in real world batteries. 2 Several methods were suggested to enhance the kinetic condition of the ion migration between the cathode and the solid electrolyte (SE). 3 A composite strategy that mixes active materials and SEs for the cathode is a general way to decrease the ion transmission barrier at the cathode-electrolyte interface. 3 The active material concentration in the cathode is reduced as much as the SE portion increases by which the energy density of the ASSB is restricted. In addition, the mixing approach generally accompanies lattice mismatches between the cathode active materials and the SE, thus providing only limited improvements, which is imputed by random contacts between the cathode active materials and the SE during the mixingmore »process. Implementing high-pressure for the electrode and electrolyte of ASSB in the assembling process has been verified is a but effective way to boost the ion transmission ability between the cathode active materials and the SE by decreasing the grain boundary impedance. Whereas the short-circuit of the battery would be induced by the mechanical deformation of the electrolyte under high pressure. 4 Herein, we demonstrate a novel way to address the ion transmission problem at the cathode-electrolyte interface in ASSBs. Starting from the cathode configuration, the finite element method (FEM) was employed to evaluate the current concentration and the distribution of the space charge layer at the cathode-electrolyte interface. Hierarchical three-dimensional (HTD) structures are found to have a higher Li + transfer number (t Li+ ), fewer free anions, and the weaker space-charge layer at the cathode-electrolyte interface in the resulting FEM simulation. To take advantage of the HTD structure, stereolithography is adopted as a manufacturing technique and single-crystalline Ni-rich (SCN) materials are selected as the active materials. Next, the manufactured HTD cathode is sintered at 600 °C in an N 2 atmosphere for the carbonization of the resin, which induces sufficient electronic conductivity for the cathode. Then, the gel-like Li 1.4 Al 0.4 Ti 1.6 (PO 4 ) 3 (LATP) precursor is synthesized and filled into the voids of the HTD structure cathode sufficiently. And the filled HTD structure cathodes are sintered at 900 °C to achieve the crystallization of the LATP gel. Scanning transmission electron microscopy (STEM) is used to unveil the morphology of the cathode-electrolyte interface between the sintered HTD cathode and the in-situ generated electrolyte (LATP). A transient phase has been found generated at the interface and matched with both lattices of the SCN and the SE, accelerating the transmission of the Li-ions, which is further verified by density functional theory calculations. In addition, Electron Energy Loss Spectroscopy demonstrates the preserved interface between HTD cathode and SEs. Atomic force microscopy is employed to measure the potential image of the cross-sectional interface by the peak force tapping mode. The average potential of modified samples is lower than the sample that mix SCN and SEs simply in the 2D planar structure, which confirms a weakened space charge layer by the enhanced contact capability as well as the ion transmission ability. To see if the demonstrated method is universally applicable, LiNi 0.8 Co 0.1 Mn 0.1 O 2 (NCM811) is selected as the cathode active material and manufactured in the same way as the SCN. The HTD cathode based on NCM811 exhibits higher electrochemical performance compared with the reference sample based on the 2D planar mixing-type cathode. We believe such a demonstrated universal strategy provides a new guideline to engineer the cathode/electrolyte interface by revolutionizing electrode structures that can be applicable to all-solid-state batteries. Figure 1. Schematic of comparing of traditional 2D planar cathode and HTD cathode in ASSB Tikekar, M. D. , et al. , Nature Energy (2016) 1 (9), 16114 Banerjee, A. , et al. , Chem Rev (2020) 120 (14), 6878 Chen, R. , et al. , Chem Rev (2020) 120 (14), 6820 Cheng, X. , et al. , Advanced Energy Materials (2018) 8 (7) Figure 1« less
  2. Metal-ion batteries (e.g., lithium and sodium ion batteries) are the promising power sources for portable electronics, electric vehicles, and smart grids. Recent metal-ion batteries with organic liquid electrolytes still suffer from safety issues regarding inflammability and insufficient lifetime.1 As the next generation energy storage devices, all-solid-state batteries (ASSBs) have promising potentials for the improved safety, higher energy density, and longer cycle life than conventional Li-ion batteries.2 The nonflammable solid electrolytes (SEs), where only Li ions are mobile, could prevent battery combustion and explosion since the side reactions that cause safety issues as well as degradation of the battery performance are largely suppressed. However, their practical application is hampered by the high resistance arising at the solid–solid electrode–electrolyte interface (including cathode-electrolyte interface and anode-electrolyte interface).3 Several methods have been introduced to optimize the contact capability as well as the electrochemical/chemical stability between the metal anodes (i.e.: Li and Na) and the SEs, which exhibited decent results in decreasing the charge transfer resistance and broadening the range of the stable energy window (i.e., lowing the chemical potential of metal anode below the highest occupied molecular orbital of the SEs).4 Nevertheless, mitigation for the cathode in ASSB is tardily developed because: (1) themore »porous structure of the cathode is hard to be infiltrated by SEs;5 (2) SEs would be oxidized and decomposed by the high valence state elements at the surface of the cathode at high state of charge.5 Herein, we demonstrate a universal cathode design strategy to achieve superior contact capability and high electrochemical/chemical stability with SEs. Stereolithography is adopted as a manufacturing technique to realize a hierarchical three-dimensional (HTD) electrode architecture with micro-size channels, which is expected to provide larger contact areas with SEs. Then, the manufactured cathode is sintered at 700 °C in a reducing atmosphere (e.g.: H2) to accomplish the carbonization of the resin, delivering sufficiently high electronic conductivity for the cathode. To avoid the direct exposure of the cathode active materials to the SEs, oxidative chemical vapor deposition technique (oCVD) is leveraged to build conformal and highly conducting poly(3,4-ethylenedioxythiophene) (PEDOT) on the surface of the HTD cathode.6 To demonstrate our design strategy, both NCM811 and Na3V2(PO4)3 is selected as active materials in the HTD cathode, then each cathode is paired with organic (polyacrylonitrile-based) and inorganic (sulfur-based) SEs assembled into two batteries (total four batteries). SEM and TEM reveal the micro-size HTD structure with built-in channels. Featured by the HTD architecture, the intrinsic kinetic and thermodynamic conditions will be enhanced by larger surface contact areas, more active sites, improved infusion and electrolyte ion accessibility, and larger volume expansion capability. Disclosed by X-ray computed tomography, the interface between cathode and SEs in the four modified samples demonstrates higher homogeneity at the interface between the cathode and SEs than that of all other pristine samples. Atomic force microscopy is employed to measure the potential image of the cross-sectional interface by the peak force tapping mode. The average potential of modified samples is lower than that of pristine samples, which confirms a weakened space charge layer by the enhanced contact capability. In addition, through Electron Energy Loss Spectroscopy coupled with Scanning Transmission Electron Microscopy, the preserved interface between HTD cathode and SE is identified; however, the decomposing of the pristine cathode is clearly observed. In addition, Finite element method simulations validate that the diffusion dynamics of lithium ions is favored by HTD structure. Such a demonstrated universal strategy provides a new guideline to engineer cathode electrolyte interface by reconstructing electrode structures that can be applicable to all solid-state batteries in a wide range of chemical conditions.« less
  3. A massive amount of data generated today on platforms such as social networks, telecommunication networks, and the internet in general can be represented as graph streams. Activity in a network’s underlying graph generates a sequence of edges in the form of a stream; for example, a social network may generate a graph stream based on the interactions (edges) between different users (nodes) over time. While many graph mining algorithms have already been developed for analyzing relatively small graphs, graphs that begin to approach the size of real-world networks stress the limitations of such methods due to their dynamic nature and the substantial number of nodes and connections involved. In this paper we present GraphZip, a scalable method for mining interesting patterns in graph streams. GraphZip is inspired by the Lempel-Ziv (LZ) class of compression algorithms, and uses a novel dictionary-based compression approach to discover maximally- compressing patterns in a graph stream. We experimentally show that GraphZip is able to retrieve complex and insightful patterns from large real-world graphs and artificially-generated graphs with ground truth patterns. Additionally, our results demonstrate that GraphZip is both highly efficient and highly effective compared to existing state-of-the-art methods for mining graph streams.
  4. Mäkelä, Annikki (Ed.)
    Abstract Climate models project warmer summer temperatures will increase the frequency and heat severity of droughts in temperate forests of Eastern North America. Hotter droughts are increasingly documented to affect tree growth and forest dynamics, with critical impacts on tree mortality, carbon sequestration and timber provision. The growing acknowledgement of the dominant role of drought timing on tree vulnerability to water deficit raises the issue of our limited understanding of radial growth phenology for most temperate tree species. Here, we use well-replicated dendrometer band data sampled frequently during the growing season to assess the growth phenology of 610 trees from 15 temperate species over 6 years. Patterns of diameter growth follow a typical logistic shape, with growth rates reaching a maximum in June, and then decreasing until process termination. On average, we find that diffuse-porous species take 16–18 days less than other wood-structure types to put on 50% of their annual diameter growth. However, their peak growth rate occurs almost a full month later than ring-porous and conifer species (ca. 24 ± 4 days; mean ± 95% credible interval). Unlike other species, the growth phenology of diffuse-porous species in our dataset is highly correlated with their spring foliar phenology. We also find that the later windowmore »of growth in diffuse-porous species, coinciding with peak evapotranspiration and lower water availability, exposes them to a higher water deficit of 88 ± 19 mm (mean ± SE) during their peak growth than ring-porous and coniferous species (15 ± 35 mm and 30 ± 30 mm, respectively). Given the high climatic sensitivity of wood formation, our findings highlight the importance of wood porosity as one predictor of species climatic sensitivity to the projected intensification of the drought regime in the coming decades.« less
  5. There has been a significant interest in applying programming-by-example to automate repetitive and tedious tasks. However, due to the incomplete nature of input-output examples, a synthesizer may generate programs that pass the examples but do not match the user intent. In this paper, we propose MARS, a novel synthesis framework that takes as input a multi-layer specification composed by input-output examples, textual description, and partial code snippets that capture the user intent. To accurately capture the user intent from the noisy and ambiguous description, we propose a hybrid model that combines the power of an LSTM-based sequence-to-sequence model with the apriori algorithm for mining association rules through unsupervised learning. We reduce the problem of solving a multi-layer specification synthesis to a Max-SMT problem, where hard constraints encode well-typed concrete programs and soft constraints encode the user intent learned by the hybrid model. We instantiate our hybrid model to the data wrangling domain and compare its performance against Morpheus, a state-of-the-art synthesizer for data wrangling tasks. Our experiments demonstrate that our approach outperforms MORPHEUS in terms of running time and solved benchmarks. For challenging benchmarks, our approach can suggest candidates with rankings that are an order of magnitude better than MORPHEUSmore »which leads to running times that are 15x faster than MORPHEUS.« less