This work aims to demonstrate that an incremental inductive model checking algorithm built on top of Boolean satisfiability (SAT) solvers can be extended to support modal mu calculus (MMC) formulas. The resulting algorithm, called modal mu calculus model checking using myopic constraints (MC3), solves MMC model checking problems over Boolean labeled transition systems (LTSs). MMC subsumes simple invariance/reachability (as solved by the IC3 algorithm), linear temporal logic (LTL, as solved by the fair algorithm), computation tree logic (CTL, as solved by IICTL), and CTL* (which in turn subsumes LTL and CTL, but was not previously supported by any incremental inductive algorithm). The algorithm is implemented in a prototype solver, mc3.
Thermoset polymers (e.g. epoxies, vulcanizable rubbers, polyurethanes, etc.) are crosslinked materials with excellent thermal, chemical, and mechanical stability; these properties make thermoset materials attractive for use in harsh applications and environments. Unfortunately, material robustness means that these materials persist in the environment with very slow degradation over long periods of time. Balancing the benefits of material performance with sustainability is a challenge in need of novel solutions. Here, we aimed to address this challenge by incorporating boronic acid-amine complexes into epoxy thermoset chemistries, facilitating degradation of the material under pH neutral to alkaline conditions; in this scenario, water acts as an initiator to remove boron species, creating a porous structure with an enhanced surface area that makes the material more amenable to environmental degradation. Furthermore, the expulsion of the boron leaves the residual pores rich in amines which can be exploited for CO2 absorption or other functionalization. We demonstrated the formation of novel boron species from neat mixing of amine compounds with boric acid, including one complex that appears highly stable under nitrogen atmosphere up to 600 °C. While degradation of the materials under static, alkaline conditions (our “trigger”) was inconclusive at the time of this writing, dynamic conditions appeared more promising. Additionally, we showed that increasing boronic acid content created materials more resistant to thermal degradation, thus improving performance under typical high temperature use conditions.
Co-deposited, immiscible alloy systems form hierarchical microstructures under specific deposition conditions that accentuate the difference in constituent element mobility. The mechanism leading to the formation of these unique hierarchical morphologies during the deposition process is difficult to identify, since the characterization of these microstructures is typically carried out post-deposition. We employ phase-field modeling to study the evolution of microstructures during deposition combined with microscopy characterization of experimentally deposited thin films to reveal the origin of the formation mechanism of hierarchical morphologies in co-deposited, immiscible alloy thin films. Our results trace this back to the significant influence of a local compositional driving force that occurs near the surface of the growing thin film. We show that local variations in the concentration of the vapor phase near the surface, resulting in nuclei (i.e., a cluster of atoms) on the film’s surface with an inhomogeneous composition, can trigger the simultaneous evolution of multiple concentration modulations across multiple length scales, leading to hierarchical morphologies. We show that locally, the concentration must be above a certain threshold value in order to generate distinct hierarchical morphologies in a single domain.
