TY - JOUR
AB - Advances in shape-morphing materials, such as hydrogels, shape-memory polymers and light-responsive polymers have enabled prescribing self-directed deformations of initially flat geometries. However, most proposed solutions evolve towards a target geometry without considering time-dependent actuation paths. To achieve more complex geometries and avoid self-collisions, it is critical to encode a spatial and temporal shape evolution within the initially flat shell. Recent realizations of time-dependent morphing are limited to the actuation of few, discrete hinges and cannot form doubly curved surfaces. Here, we demonstrate a method for encoding temporal shape evolution in architected shells that assume complex shapes and doubly curved geometries. The shells are non-periodic tessellations of pre-stressed contractile unit cells that soften in water at rates prescribed locally by mesostructure geometry. The ensuing midplane contraction is coupled to the formation of encoded curvatures. We propose an inverse design tool based on a data-driven model for unit cellsâ€™ temporal responses.
AU - Guseinov, Ruslan
AU - McMahan, Connor
AU - Perez Rodriguez, Jesus
AU - Daraio, Chiara
AU - Bickel, Bernd
ID - 7262
JF - Nature Communications
KW - Design
KW - Synthesis and processing
KW - Mechanical engineering
KW - Polymers
SN - 2041-1723
TI - Programming temporal morphing of self-actuated shells
VL - 11
ER -
TY - CONF
AB - We present two algorithmic approaches for synthesizing linear hybrid automata from experimental data. Unlike previous approaches, our algorithms work without a template and generate an automaton with nondeterministic guards and invariants, and with an arbitrary number and topology of modes. They thus construct a succinct model from the data and provide formal guarantees. In particular, (1) the generated automaton can reproduce the data up to a specified tolerance and (2) the automaton is tight, given the first guarantee. Our first approach encodes the synthesis problem as a logical formula in the theory of linear arithmetic, which can then be solved by an SMT solver. This approach minimizes the number of modes in the resulting model but is only feasible for limited data sets. To address scalability, we propose a second approach that does not enforce to find a minimal model. The algorithm constructs an initial automaton and then iteratively extends the automaton based on processing new data. Therefore the algorithm is well-suited for online and synthesis-in-the-loop applications. The core of the algorithm is a membership query that checks whether, within the specified tolerance, a given data set can result from the execution of a given automaton. We solve this membership problem for linear hybrid automata by repeated reachability computations. We demonstrate the effectiveness of the algorithm on synthetic data sets and on cardiac-cell measurements.
AU - Garcia Soto, Miriam
AU - Henzinger, Thomas A
AU - Schilling, Christian
AU - Zeleznik, Luka
ID - 6493
KW - Synthesis
KW - Linear hybrid automaton
KW - Membership
SN - 0302-9743
T2 - 31st International Conference on Computer-Aided Verification
TI - Membership-based synthesis of linear hybrid automata
VL - 11561
ER -