Computer Engineering Commons^™

Low-Energy Acceleration Of Binarized Convolutional Neural Networks Using A Spin Hall Effect Based Logic-In-Memory Architecture, Ashkan Samiee, Payal Borulkar, Ronald F. Demara, Peiyi Zhao, Yu Bai

Engineering Faculty Articles and Research

Deep Learning (DL) offers the advantages of high accuracy performance at tasks such as image recognition, learning of complex intelligent behaviors, and large-scale information retrieval problems such as intelligent web search. To attain the benefits of DL, the high computational and energy-consumption demands imposed by the underlying processing, interconnect, and memory devices on which software-based DL executes can benefit substantially from innovative hardware implementations. Logic-in-Memory (LIM) architectures offer potential approaches to attaining such throughput goals within area and energy constraints starting with the lowest layers of the hardware stack. In this paper, we develop a Spintronic Logic-in-Memory (S-LIM) XNOR neural …

Paper Prototyping Comfortable Vr Play For Diverse Sensory Needs, Louanne E. Boyd, Kendra Day, Ben Wasserman, Kaitlyn Abdo, Gillian Hayes, Erik J. Linstead

Engineering Faculty Articles and Research

We co-designed paper prototype dashboards for virtual environments for three children with diverse sensory needs. Our goal was to determine individual interaction styles in order to enable comfortable and inclusive play. As a first step towards an inclusive virtual world, we began with designing for three sensory-diverse children who have labels of neurotypical, ADHD, and autism respectively. We focused on their leisure interests and their individual sensory profiles. We present the results of co-design with family members and paper prototyping sessions conducted by family members with the children. The results contribute preliminary empirical findings for accommodating different levels of engagement …

Applications Of Supervised Machine Learning In Autism Spectrum Disorder Research: A Review, Kayleigh K. Hyde, Marlena N. Novack, Nicholas Lahaye, Chelsea Parlett-Pelleriti, Raymond Anden, Dennis R. Dixon, Erik Linstead

Engineering Faculty Articles and Research

Autism spectrum disorder (ASD) research has yet to leverage "big data" on the same scale as other fields; however, advancements in easy, affordable data collection and analysis may soon make this a reality. Indeed, there has been a notable increase in research literature evaluating the effectiveness of machine learning for diagnosing ASD, exploring its genetic underpinnings, and designing effective interventions. This paper provides a comprehensive review of 45 papers utilizing supervised machine learning in ASD, including algorithms for classification and text analysis. The goal of the paper is to identify and describe supervised machine learning trends in ASD literature as …

Exploring Age-Related Metamemory Differences Using Modified Brier Scores And Hierarchical Clustering, Chelsea Parlett-Pelleriti, Grace C. Lin, Masha R. Jones, Erik Linstead, Susanne M. Jaeggi

Engineering Faculty Articles and Research

Older adults (OAs) typically experience memory failures as they age. However, with some exceptions, studies of OAs’ ability to assess their own memory functions—Metamemory (MM)— find little evidence that this function is susceptible to age-related decline. Our study examines OAs’ and young adults’ (YAs) MM performance and strategy use. Groups of YAs (N = 138) and OAs (N = 79) performed a MM task that required participants to place bets on how likely they were to remember words in a list. Our analytical approach includes hierarchical clustering, and we introduce a new measure of MM—the modified Brier—in order to adjust …

Prototype Of A Fish Inspired Swimming Silk Robot, Cassandra M. Donatelli, Sarah A. Bradner, Juanita Mathews, Erin Sanders, Casey R. Culligan, David Kaplan, Eric D. Tytell

Engineering Faculty Articles and Research

Elongate fishes have evolved hundreds of times throughout the tree of life. They occupy many aquatic environments, from streams and ponds to the deepest parts of the ocean. Due to their long body and numerous vertebrae, they are also highly flexible animals, which makes them useful as bioinspiration for designs in the field of soft robotics. We present a biodegradable soft robot prototype, inspired by elongate fishes. The robot's body is primarily composed of a silk hydrogel with embedded fibers to mimic the structure of natural fish skin. When actuated at the front, the flexible gel prototype mimics the undulatory …

Multiple-Change-Point Modeling And Exact Bayesian Inference Of Degradation Signal For Prognostic Improvement, Yuxin Wen, Jianguo Wu, Qiang Matthew Zhou, Tzu-Liang Bill Tseng

Engineering Faculty Articles and Research

Prognostics play an increasingly important role in modern engineering systems for smart maintenance decision-making. In parametric regression-based approaches, the parametric models are often too rigid to model degradation signals in many applications. In this paper, we propose a Bayesian multiple-change-point (CP) modeling framework to better capture the degradation path and improve the prognostics. At the offline modeling stage, a novel stochastic process is proposed to model the joint prior of CPs and positions. All hyperparameters are estimated through an empirical two-stage process. At the online monitoring and remaining useful life (RUL) prediction stage, a recursive updating algorithm is developed to …

Degradation Modeling And Rul Prediction Using Wiener Process Subject To Multiple Change Points And Unit Heterogeneity, Yuxin Wen, Jianguo Wu, Devashish Das, Tzu-Liang Bill Tseng

Engineering Faculty Articles and Research

Degradation modeling is critical for health condition monitoring and remaining useful life prediction (RUL). The prognostic accuracy highly depends on the capability of modeling the evolution of degradation signals. In many practical applications, however, the degradation signals show multiple phases, where the conventional degradation models are often inadequate. To better characterize the degradation signals of multiple-phase characteristics, we propose a multiple change-point Wiener process as a degradation model. To take into account the between-unit heterogeneity, a fully Bayesian approach is developed where all model parameters are assumed random. At the offline stage, an empirical two-stage process is proposed for model …

Soft Foam Robot With Caterpillar-Inspired Gait Regimes For Terrestrial Locomotion, Cassandra M. Donatelli, Zachary T. Serlin, Piers Echols-Jones, Anthony E. Scibelli, Alexandra Cohen, Jeanne-Marie Musca, Shane Rozen-Levy, David Buckingham, Robert White, Barry A. Trimmer

Engineering Faculty Articles and Research

Caterpillars are the soft bodied larvae of lepidopteran insects. They have evolved to occupy an extremely diverse range of natural environments and to locomote in complex three-dimensional structures without articulated joint or hydrostatic control. These animals make excellent bio-inspiration for the field of soft robotics because of their diversity and adaptability. In this paper, we present SquMA Bot, a caterpillar-inspired soft robot. The robot's body is primarily composed of a soft viscoelastic foam, and it is actuated using a motor-tendon system. SquMA Bot is able to mimic the inching gait of a caterpillar and can use its flexible body to …

Multiple-Phase Modeling Of Degradation Signal For Condition Monitoring And Remaining Useful Life Prediction, Yuxin Wen, Jianguo Wu, Yuan Yuan

Engineering Faculty Articles and Research

Remaining useful life prediction plays an important role in ensuring the safety, availability, and efficiency of various engineering systems. In this paper, we propose a flexible Bayesian multiple-phase modeling approach to characterize degradation signals for prognosis. The priors are specified with a novel stochastic process and the multiple-phase model is formulated to a novel state-space model to facilitate online monitoring and prediction. A particle filtering algorithm with stratified sampling and partial Gibbs resample-move strategy is developed for online model updating and residual life prediction. The advantages of the proposed method are demonstrated through extensive numerical studies and real case studies.

Features Of Agent-Based Models, Reiko Heckel, Alexander Kurz, Edmund Chattoe-Brown

Engineering Faculty Articles and Research

The design of agent-based models (ABMs) is often ad-hoc when it comes to defining their scope. In order for the inclusion of features such as network structure, location, or dynamic change to be justified, their role in a model should be systematically analysed. We propose a mechanism to compare and assess the impact of such features. In particular we are using techniques from software engineering and semantics to support the development and assessment of ABMs, such as graph transformations as semantic representations for agent-based models, feature diagrams to identify ingredients under consideration, and extension relations between graph transformation systems to …

The Positivication Of Coalgebraic Logics, Fredrik Dahlqvist, Alexander Kurz

Engineering Faculty Articles and Research

We present positive coalgebraic logic in full generality, and show how to obtain a positive coalgebraic logic from a boolean one. On the model side this involves canonically computing a endofunctor T': Pos->Pos from an endofunctor T: Set->Set, in a procedure previously defined by the second author et alii called posetification. On the syntax side, it involves canonically computing a syntax-building functor L': DL->DL from a syntax-building functor L: BA->BA, in a dual procedure which we call positivication. These operations are interesting in their own right and we explicitly compute posetifications and positivications in the case …

Foreword: Special Issue On Coalgebraic Logic, Alexander Kurz

Engineering Faculty Articles and Research

The second Dagstuhl seminar on coalgebraic logics took place from October 7-12, 2012, in the Leibniz Forschungszentrum Schloss Dagstuhl, following a successful earlier one in December 2009. From the 44 researchers who attended and the 30 talks presented, this collection highlights some of the progress that has been made in the field. We are grateful to Giuseppe Longo and his interest in a special issue in Mathematical Structures in Computer Science.

Quasivarieties And Varieties Of Ordered Algebras: Regularity And Exactness, Alexander Kurz

Engineering Faculty Articles and Research

We characterise quasivarieties and varieties of ordered algebras categorically in terms of regularity, exactness and the existence of a suitable generator. The notions of regularity and exactness need to be understood in the sense of category theory enriched over posets.

We also prove that finitary varieties of ordered algebras are cocompletions of their theories under sifted colimits (again, in the enriched sense).

Tool Support For Reasoning In Display Calculi, Samuel Balco, Sabine Frittella, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano

Engineering Faculty Articles and Research

We present a tool for reasoning in and about propositional sequent calculi. One aim is to support reasoning in calculi that contain a hundred rules or more, so that even relatively small pen and paper derivations become tedious and error prone. As an example, we implement the display calculus D.EAK of dynamic epistemic logic. Second, we provide embeddings of the calculus in the theorem prover Isabelle for formalising proofs about D.EAK. As a case study we show that the solution of the muddy children puzzle is derivable for any number of muddy children. Third, there is a set of meta-tools, …

Multi-Type Display Calculus For Dynamic Epistemic Logic, Sabine Frittella, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano, Vlasta Sikimić

Engineering Faculty Articles and Research

In the present paper, we introduce a multi-type display calculus for dynamic epistemic logic, which we refer to as Dynamic Calculus. The displayapproach is suitable to modularly chart the space of dynamic epistemic logics on weaker-than-classical propositional base. The presence of types endows the language of the Dynamic Calculus with additional expressivity, allows for a smooth proof-theoretic treatment, and paves the way towards a general methodology for the design of proof systems for the generality of dynamic logics, and certainly beyond dynamic epistemic logic. We prove that the Dynamic Calculus adequately captures Baltag-Moss-Solecki’s dynamic epistemic logic, and enjoys Belnap-style cut …

Multi-Type Display Calculus For Propositional Dynamic Logic, Sabine Frittella, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano

Engineering Faculty Articles and Research

We introduce a multi-type display calculus for Propositional Dynamic Logic (PDL). This calculus is complete w.r.t. PDL, and enjoys Belnap-style cut-elimination and subformula property.

Extensions Of Functors From Set To V-Cat, Adriana Balan, Alexander Kurz, Jirí Velebil

Engineering Faculty Articles and Research

We show that for a commutative quantale V every functor Set --> V-cat has an enriched left- Kan extension. As a consequence, coalgebras over Set are subsumed by coalgebras over V-cat. Moreover, one can build functors on V-cat by equipping Set-functors with a metric.

Approximation Of Nested Fixpoints, Alexander Kurz

Engineering Faculty Articles and Research

The question addressed in this paper is how to correctly approximate infinite data given by systems of simultaneous corecursive definitions. We devise a categorical framework for reasoning about regular datatypes, that is, datatypes closed under products, coproducts and fixpoints. We argue that the right methodology is on one hand coalgebraic (to deal with possible nontermination and infinite data) and on the other hand 2-categorical (to deal with parameters in a disciplined manner). We prove a coalgebraic version of Bekic lemma that allows us to reduce simultaneous fixpoints to a single fix point. Thus a possibly infinite object of interest is …

Coalgebraic Semantics Of Reflexive Economics (Dagstuhl Seminar 15042), Samson Abramsky, Alexander Kurz, Pierre Lescanne, Viktor Winschel

Engineering Faculty Articles and Research

This report documents the program and the outcomes of Dagstuhl Seminar 15042 “Coalgebraic Semantics of Reflexive Economics”.

Positive Fragments Of Coalgebraic Logics, Adriana Balan, Alexander Kurz, Jirí Velebil

Engineering Faculty Articles and Research

Positive modal logic was introduced in an influential 1995 paper of Dunn as the positive fragment of standard modal logic. His completeness result consists of an axiomatization that derives all modal formulas that are valid on all Kripke frames and are built only from atomic propositions, conjunction, disjunction, box and diamond. In this paper, we provide a coalgebraic analysis of this theorem, which not only gives a conceptual proof based on duality theory, but also generalizes Dunn's result from Kripke frames to coalgebras for weak-pullback preserving functors. To facilitate this analysis we prove a number of category theoretic results on …

Presenting Distributive Laws, Marcello M. Bonsangue, Helle H. Hansen, Alexander Kurz, Jurriaan Rot

Engineering Faculty Articles and Research

Distributive laws of a monad T over a functor F are categorical tools for specifying algebra-coalgebra interaction. They proved to be important for solving systems of corecursive equations, for the specification of well-behaved structural operational semantics and, more recently, also for enhancements of the bisimulation proof method. If T is a free monad, then such distributive laws correspond to simple natural transformations. However, when T is not free it can be rather difficult to prove the defining axioms of a distributive law. In this paper we describe how to obtain a distributive law for a monad with an equational presentation …

A Proof-Theoretic Semantic Analysis Of Dynamic Epistemic Logic, Sabine Frittella, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano, Vlasta Sikimić

Engineering Faculty Articles and Research

The present paper provides an analysis of the existing proof systems for dynamic epistemic logic from the viewpoint of proof-theoretic semantics. Dynamic epistemic logic is one of the best known members of a family of logical systems which have been successfully applied to diverse scientific disciplines, but the proof theoretic treatment of which presents many difficulties. After an illustration of the proof-theoretic semantic principles most relevant to the treatment of logical connectives, we turn to illustrating the main features of display calculi, a proof-theoretic paradigm which has been successfully employed to give a proof-theoretic semantic account of modal and substructural …

Dynamic Sequent Calculus For The Logic Of Epistemic Actions And Knowledge, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano

Engineering Faculty Articles and Research

"Dynamic Logics (DLs) form a large family of nonclassical logics, and perhaps the one enjoying the widest range of applications. Indeed, they are designed to formalize change caused by actions of diverse nature: updates on the memory state of a computer, displacements of moving robots in an environment, measurements in models of quantum physics, belief revisions, knowledge updates, etc. In each of these areas, DL-formulas express properties of the model encoding the present state of affairs, as well as the pre- and post-conditions of a given action. Actions are semantically represented as transformations of one model into another, encoding the …

Nominal Regular Expressions For Languages Over Infinite Alphabets, Alexander Kurz, Tomoyuki Suzuki, Emilio Tuosto

Engineering Faculty Articles and Research

We propose regular expressions to abstractly model and study properties of resource-aware computations. Inspired by nominal techniques – as those popular in process calculi – we extend classical regular expressions with names (to model computational resources) and suitable operators (for allocation, deallocation, scoping of, and freshness conditions on resources). We discuss classes of such nominal regular expressions, show how such expressions have natural interpretations in terms of languages over infinite alphabets, and give Kleene theorems to characterise their formal languages in terms of nominal automata.

Nominal Computation Theory (Dagstuhl Seminar 13422), Mikołaj Bojanczyk, Bartek Klin, Alexander Kurz, Andrew M. Pitts

Engineering Faculty Articles and Research

This report documents the program and the outcomes of Dagstuhl Seminar 13422 “Nominal Computation Theory”. The underlying theme of the seminar was nominal sets (also known as sets with atoms or Fraenkel-Mostowski sets) and they role and applications in three distinct research areas: automata over infinite alphabets, program semantics using nominal sets and nominal calculi of concurrent processes.

Relation Lifting, With An Application To The Many-Valued Cover Modality, Marta Bílková, Alexander Kurz, Daniela Petrişan, Jirí Velebil

Engineering Faculty Articles and Research

We introduce basic notions and results about relation liftings on categories enriched in a commutative quantale. We derive two necessary and sufficient conditions for a 2-functor T to admit a functorial relation lifting: one is the existence of a distributive law of T over the “powerset monad” on categories, one is the preservation by T of “exactness” of certain squares. Both characterisations are generalisations of the “classical” results known for set functors: the first characterisation generalises the existence of a distributive law over the genuine powerset monad, the second generalises preservation of weak pullbacks.

The results presented in this paper …

Epistemic Updates On Algebras, Alexander Kurz, Alessandra Palmigiano

Engineering Faculty Articles and Research

We develop the mathematical theory of epistemic updates with the tools of duality theory. We focus on the Logic of Epistemic Actions and Knowledge (EAK), introduced by Baltag-Moss-Solecki, without the common knowledge operator. We dually characterize the product update construction of EAK as a certain construction transforming the complex algebras associated with the given model into the complex algebra associated with the updated model. This dual characterization naturally generalizes to much wider classes of algebras, which include, but are not limited to, arbitrary BAOs and arbitrary modal expansions of Heyting algebras (HAOs). As an application of this dual characterization, we …

Nominal Coalgebraic Data Types With Applications To Lambda Calculus, Alexander Kurz, Daniela Petrişan, Paula Severi, Fer-Jan De Vries

Engineering Faculty Articles and Research

We investigate final coalgebras in nominal sets. This allows us to define types of infinite data with binding for which all constructions automatically respect alpha equivalence. We give applications to the infinitary lambda calculus.

Strongly Complete Logics For Coalgebras, Alexander Kurz, Jiří Rosický

Engineering Faculty Articles and Research

Coalgebras for a functor model different types of transition systems in a uniform way. This paper focuses on a uniform account of finitary logics for set-based coalgebras. In particular, a general construction of a logic from an arbitrary set-functor is given and proven to be strongly complete under additional assumptions. We proceed in three parts.

Part I argues that sifted colimit preserving functors are those functors that preserve universal algebraic structure. Our main theorem here states that a functor preserves sifted colimits if and only if it has a finitary presentation by operations and equations. Moreover, the presentation of the …

Completeness For The Coalgebraic Cover Modality, Clemens Kupke, Alexander Kurz, Yde Venema

Engineering Faculty Articles and Research

We study the finitary version of the coalgebraic logic introduced by L. Moss. The syntax of this logic, which is introduced uniformly with respect to a coalgebraic type functor, required to preserve weak pullbacks, extends that of classical propositional logic with a so-called coalgebraic cover modality depending on the type functor. Its semantics is defined in terms of a categorically defined relation lifting operation.

As the main contributions of our paper we introduce a derivation system, and prove that it provides a sound and complete axiomatization for the collection of coalgebraically valid inequalities. Our soundness and completeness proof is algebraic, …