@book{3300, abstract = {This book first explores the origins of this idea, grounded in theoretical work on temporal logic and automata. The editors and authors are among the world's leading researchers in this domain, and they contributed 32 chapters representing a thorough view of the development and application of the technique. Topics covered include binary decision diagrams, symbolic model checking, satisfiability modulo theories, partial-order reduction, abstraction, interpolation, concurrency, security protocols, games, probabilistic model checking, and process algebra, and chapters on the transfer of theory to industrial practice, property specification languages for hardware, and verification of real-time systems and hybrid systems. The book will be valuable for researchers and graduate students engaged with the development of formal methods and verification tools.}, author = {Clarke, Edmund M. and Henzinger, Thomas A and Veith, Helmut and Bloem, Roderick}, isbn = {978-3-319-10574-1}, pages = {XLVIII, 1212}, publisher = {Springer Nature}, title = {{Handbook of Model Checking}}, doi = {10.1007/978-3-319-10575-8}, year = {2018}, } @inbook{37, abstract = {Developmental processes are inherently dynamic and understanding them requires quantitative measurements of gene and protein expression levels in space and time. While live imaging is a powerful approach for obtaining such data, it is still a challenge to apply it over long periods of time to large tissues, such as the embryonic spinal cord in mouse and chick. Nevertheless, dynamics of gene expression and signaling activity patterns in this organ can be studied by collecting tissue sections at different developmental stages. In combination with immunohistochemistry, this allows for measuring the levels of multiple developmental regulators in a quantitative manner with high spatiotemporal resolution. The mean protein expression levels over time, as well as embryo-to-embryo variability can be analyzed. A key aspect of the approach is the ability to compare protein levels across different samples. This requires a number of considerations in sample preparation, imaging and data analysis. Here we present a protocol for obtaining time course data of dorsoventral expression patterns from mouse and chick neural tube in the first 3 days of neural tube development. The described workflow starts from embryo dissection and ends with a processed dataset. Software scripts for data analysis are included. The protocol is adaptable and instructions that allow the user to modify different steps are provided. Thus, the procedure can be altered for analysis of time-lapse images and applied to systems other than the neural tube.}, author = {Zagórski, Marcin P and Kicheva, Anna}, booktitle = {Morphogen Gradients }, isbn = {978-1-4939-8771-9}, issn = {1064-3745}, pages = {47 -- 63}, publisher = {Springer Nature}, title = {{Measuring dorsoventral pattern and morphogen signaling profiles in the growing neural tube}}, doi = {10.1007/978-1-4939-8772-6_4}, volume = {1863}, year = {2018}, } @article{398, abstract = {Objective: To report long-term results after Pipeline Embolization Device (PED) implantation, characterize complex and standard aneurysms comprehensively, and introduce a modified flow disruption scale. Methods: We retrospectively reviewed a consecutive series of 40 patients harboring 59 aneurysms treated with 54 PEDs. Aneurysm complexity was assessed using our proposed classification. Immediate angiographic results were analyzed using previously published grading scales and our novel flow disruption scale. Results: According to our new definition, 46 (78%) aneurysms were classified as complex. Most PED interventions were performed in the paraophthalmic and cavernous internal carotid artery segments. Excellent neurologic outcome (modified Rankin Scale 0 and 1) was observed in 94% of patients. Our data showed low permanent procedure-related mortality (0%) and morbidity (3%) rates. Long-term angiographic follow-up showed complete occlusion in 81% and near-total obliteration in a further 14%. Complete obliteration after deployment of a single PED was achieved in all standard aneurysms with 1-year follow-up. Our new scale was an independent predictor of aneurysm occlusion in a multivariable analysis. All aneurysms with a high flow disruption grade showed complete occlusion at follow-up regardless of PED number or aneurysm complexity. Conclusions: Treatment with the PED should be recognized as a primary management strategy for a highly selected cohort with predominantly complex intracranial aneurysms. We further show that a priori assessment of aneurysm complexity and our new postinterventional angiographic flow disruption scale predict occlusion probability and may help to determine the adequate number of per-aneurysm devices.}, author = {Dodier, Philippe and Frischer, Josa and Wang, Wei and Auzinger, Thomas and Mallouhi, Ammar and Serles, Wolfgang and Gruber, Andreas and Knosp, Engelbert and Bavinzski, Gerhard}, journal = {World Neurosurgery}, pages = {e568--e578}, publisher = {Elsevier}, title = {{Immediate flow disruption as a prognostic factor after flow diverter treatment long term experience with the pipeline embolization device}}, doi = {10.1016/j.wneu.2018.02.096}, volume = {13}, year = {2018}, } @article{407, abstract = {Isoprenoid cytokinins play a number of crucial roles in the regulation of plant growth and development. To study cytokinin receptor properties in plants, we designed and prepared fluorescent derivatives of 6-[(3-methylbut-2-en-1-yl)amino]purine (N6-isopentenyladenine, iP) with several fluorescent labels attached to the C2 or N9 atom of the purine moiety via a 2- or 6-carbon linker. The fluorescent labels included dansyl (DS), fluorescein (FC), 7-nitrobenzofurazan (NBD), rhodamine B (RhoB), coumarin (Cou), 7-(diethylamino)coumarin (DEAC) and cyanine 5 dye (Cy5). All prepared compounds were screened for affinity for the Arabidopsis thaliana cytokinin receptor (CRE1/AHK4). Although the attachment of the fluorescent labels to iP via the linkers mostly disrupted binding to the receptor, several fluorescent derivatives interacted well. For this reason, three derivatives, two rhodamine B and one 4-chloro-7-nitrobenzofurazan labeled iP were tested for their interaction with CRE1/AHK4 and Zea mays cytokinin receptors in detail. We further showed that the three derivatives were able to activate transcription of cytokinin response regulator ARR5 in Arabidopsis seedlings. The activity of fluorescently labeled cytokinins was compared with corresponding 6-dimethylaminopurine fluorescently labeled negative controls. Selected rhodamine B C2-labeled compounds 17, 18 and 4-chloro-7-nitrobenzofurazan N9-labeled compound 28 and their respective negative controls (19, 20 and 29, respectively) were used for in planta staining experiments in Arabidopsis thaliana cell suspension culture using live cell confocal microscopy.}, author = {Kubiasová, Karolina and Mik, Václav and Nisler, Jaroslav and Hönig, Martin and Husičková, Alexandra and Spíchal, Lukáš and Pěkná, Zuzana and Šamajová, Olga and Doležal, Karel and Plíhal, Ondřej and Benková, Eva and Strnad, Miroslav and Plíhalová, Lucie}, journal = {Phytochemistry}, pages = {1--11}, publisher = {Elsevier}, title = {{Design, synthesis and perception of fluorescently labeled isoprenoid cytokinins}}, doi = {10.1016/j.phytochem.2018.02.015}, volume = {150}, year = {2018}, } @article{425, abstract = {We show that the following algorithmic problem is decidable: given a 2-dimensional simplicial complex, can it be embedded (topologically, or equivalently, piecewise linearly) in R3? By a known reduction, it suffices to decide the embeddability of a given triangulated 3-manifold X into the 3-sphere S3. The main step, which allows us to simplify X and recurse, is in proving that if X can be embedded in S3, then there is also an embedding in which X has a short meridian, that is, an essential curve in the boundary of X bounding a disk in S3 \ X with length bounded by a computable function of the number of tetrahedra of X.}, author = {Matoušek, Jiří and Sedgwick, Eric and Tancer, Martin and Wagner, Uli}, journal = {Journal of the ACM}, number = {1}, publisher = {ACM}, title = {{Embeddability in the 3-Sphere is decidable}}, doi = {10.1145/3078632}, volume = {65}, year = {2018}, } @inproceedings{433, abstract = {A thrackle is a graph drawn in the plane so that every pair of its edges meet exactly once: either at a common end vertex or in a proper crossing. We prove that any thrackle of n vertices has at most 1.3984n edges. Quasi-thrackles are defined similarly, except that every pair of edges that do not share a vertex are allowed to cross an odd number of times. It is also shown that the maximum number of edges of a quasi-thrackle on n vertices is 3/2(n-1), and that this bound is best possible for infinitely many values of n.}, author = {Fulek, Radoslav and Pach, János}, location = {Boston, MA, United States}, pages = {160 -- 166}, publisher = {Springer}, title = {{Thrackles: An improved upper bound}}, doi = {10.1007/978-3-319-73915-1_14}, volume = {10692}, year = {2018}, } @article{17575, abstract = {Black hole (BH) mergers detectable with the Laser Interferometer Gravitational-wave Observatory (LIGO) can occur in active galactic nucleus (AGN) disks. Here we parameterize the merger rates, the mass spectrum, and the spin spectrum of BHs in AGN disks. The predicted merger rate spans ∼10−3–104 Gpc−1 yr−1, so upper limits from LIGO (<212 Gpc−1 yr−1) already constrain it. The predicted mass spectrum has the form of a broken power law, consisting of a pre-existing BH power-law mass spectrum and a harder power-law mass spectrum resulting from mergers. The predicted spin spectrum is multipeaked with the evolution of retrograde spin BHs in the gas disk playing a key role. We outline the large uncertainties in each of these LIGO observables for this channel and we discuss ways in which they can be constrained in the future.}, author = {McKernan, Barry and Saavik Ford, K. E. and Bellovary, J. and Leigh, N. W. C. and Haiman, Zoltán and Kocsis, B. and Lyra, W. and Mac Low, M.-M. and Metzger, B. and O’Dowd, M. and Endlich, S. and Rosen, D. J.}, issn = {0004-637X}, journal = {The Astrophysical Journal}, number = {1}, publisher = {American Astronomical Society}, title = {{Constraining stellar-mass black hole mergers in AGN disks detectable with LIGO}}, doi = {10.3847/1538-4357/aadae5}, volume = {866}, year = {2018}, } @article{17640, abstract = {Gravitational waves (GWs) in the nano-hertz band are great tools for understanding the cosmological evolution of supermassive black holes (SMBHs) in galactic nuclei. We consider SMBH binaries in high-z ultra-luminous infrared galaxies (ULIRGs) as sources of a stochastic GW background (GWB). ULIRGs are likely associated with gas-rich galaxy mergers containing SMBHs that possibly occur at most once in the life of galaxies, unlike multiple dry mergers at low redshift. Adopting a well-established sample of ULIRGs, we study the properties of the GWB due to coalescing binary SMBHs in these galaxies. Since the ULIRG population peaks at z>1.5, the amplitude of the GWB is not affected even if BH mergers are delayed by as long as ∼ 10 Gyrs. Despite the rarity of the high-z ULIRGs, we find a tension with the upper limits from Pulsar Timing Array (PTA) experiments. This result suggests that if a fraction fm,gal of ULIRGs are associated with SMBH binaries, then no more than 20fm,gal(λEdd/0.3)5/3(tlife/30 Myr) % of the binary SMBHs in ULIRGs can merge within a Hubble time, for plausible values of the Eddington ratio of ULIRGs (λEdd) and their lifetime (tlife).}, author = {Inayoshi, Kohei and Ichikawa, Kohei and Haiman, Zoltán}, issn = {2041-8205}, journal = {The Astrophysical Journal Letters}, number = {2}, publisher = {American Astronomical Society}, title = {{Gravitational waves from supermassive black hole binaries in ultraluminous infrared galaxies}}, doi = {10.3847/2041-8213/aad8ad}, volume = {863}, year = {2018}, } @article{17679, abstract = {We study low-density axisymmetric accretion flows onto black holes (BHs) with two-dimensional hydrodynamical simulations, adopting the α-viscosity prescription. When the gas angular momentum is low enough to form a rotationally supported disk within the Bondi radius (RB), we find a global steady accretion solution. The solution consists of a rotational equilibrium distribution at r∼RB, where the density follows ρ∝(1+RB/r)^3/2, surrounding a geometrically thick and optically thin accretion disk at the centrifugal radius, where thermal energy generated by viscosity is transported via strong convection. Physical properties of the inner solution agree with those expected in convection-dominated accretion flows (CDAF; ρ∝r^−1/2). In the inner CDAF solution, the gas inflow rate decreases towards the center due to convection (M˙∝r), and the net accretion rate (including both inflows and outflows) is strongly suppressed by several orders of magnitude from the Bondi accretion rate M˙B The net accretion rate depends on the viscous strength, following M˙/M˙B∝(α/0.01)^0.6. This solution holds for low accretion rates of M˙B/M˙Edd<10^−3 having minimal radiation cooling, where M˙Edd is the Eddington rate. In a hot plasma at the bottom (r<10^−3 RB), thermal conduction would dominate the convective energy flux. Since suppression of the accretion by convection ceases, the final BH feeding rate is found to be M˙/M˙B∼10^−3−10^−2. This rate is as low as M˙/M˙Edd∼10^−7−10^−6 inferred for SgrA∗ and the nuclear BHs in M31 and M87, and can explain the low luminosities in these sources, without invoking any feedback mechanism.}, author = {Inayoshi, Kohei and Ostriker, Jeremiah P and Haiman, Zoltán and Kuiper, Rolf}, issn = {0035-8711}, journal = {Monthly Notices of the Royal Astronomical Society}, number = {1}, pages = {1412--1426}, publisher = {Oxford University Press}, title = {{Low-density, radiatively inefficient rotating-accretion flow on to a black hole}}, doi = {10.1093/mnras/sty276}, volume = {476}, year = {2018}, } @article{17687, abstract = {We propose the formation of massive pristine dark-matter (DM) halos with masses of ∼10^8 M⊙, due to the dynamical effects of frequent mergers in rare regions of the Universe with high baryonic streaming velocity relative to DM. Since the streaming motion prevents gas collapse into DM halos and delays prior star formation episodes, the gas remains metal-free until the halo virial temperatures ≳2×10^4 K. The minimum cooling mass of DM halos is boosted by a factor of ∼10−30 because frequent major mergers of halos further inhibit gas collapse. We use Monte Carlo merger trees to simulate the DM assembly history under a streaming velocity of twice the root-mean-square value, and estimate the number density of massive DM halos containing pristine gas as ≃10^−4 cMpc^−3. When the gas infall begins, efficient Lyα cooling drives cold streams penetrating inside the halo and feeding a central galactic disk. When one stream collides with the disk, strong shock forms a dense and hot gas cloud, where the gas never forms H2 molecules due to effective collisional dissociation. As a result, a massive gas cloud forms by gravitational instability and collapses directly into a massive black hole (BH) with M∙∼10^5 M⊙. Almost simultaneously, a galaxy with M⋆,tot∼10^6 M⊙ composed of Population III stars forms in the nuclear region. If the typical stellar mass is as high as ∼100 M⊙, the galaxy could be detected with the James Webb Space Telescope even at z≳15. These massive seed BHs would be fed by continuous gas accretion from the host galaxy, and grow to be bright quasars observed at z≳6.}, author = {Inayoshi, Kohei and Li, Miao and Haiman, Zoltán}, issn = {0035-8711}, journal = {Monthly Notices of the Royal Astronomical Society}, number = {3}, pages = {4017--4027}, publisher = {Oxford University Press}, title = {{Massive black hole and Population III galaxy formation in overmassive dark-matter haloes with violent merger histories}}, doi = {10.1093/mnras/sty1720}, volume = {479}, year = {2018}, } @inproceedings{18282, abstract = {In this paper, we introduce a random forest semantic hashing scheme that embeds tiny convolutional neural networks (CNN) into shallow random forests. A binary hash code for a data point is obtained by a set of decision trees, setting ‘1’ for the visited tree leaf, and ‘0’ for the rest. We propose to first randomly group arriving classes at each tree split node into two groups, obtaining a significantly simplified two-class classification problem that can be a handled with a light-weight CNN weak learner. Code uniqueness is achieved via the random class grouping, whilst code consistency is achieved using a low-rank loss in the CNN weak learners that encourages intra-class compactness for the two random class groups. Finally, we introduce an information-theoretic approach for aggregating codes of individual trees into a single hash code, producing a near-optimal unique hash for each class. The proposed approach significantly outperforms state-of-the-art hashing methods for image retrieval tasks on large-scale public datasets, and is comparable to image classification methods while utilizing a more compact, efficient and scalable representation. This work proposes a principled and robust procedure to train and deploy in parallel an ensemble of light-weight CNNs, instead of simply going deeper.}, author = {Qiu, Qiang and Lezama, José and Bronstein, Alexander and Sapiro, Guillermo}, booktitle = {European Conference on Computer Vision}, isbn = {9783030012151}, issn = {1611-3349}, location = {Munich, Germany}, number = {Part II}, publisher = {Springer Nature}, title = {{ForestHash: Semantic hashing with shallow random forests and tiny convolutional networks}}, doi = {10.1007/978-3-030-01216-8_27}, volume = {11206}, year = {2018}, } @inproceedings{18283, abstract = {Cardiac ultrasound imaging requires a high frame rate in order to capture rapid motion. This can be achieved by multi-line acquisition (MLA), where several narrow-focused received lines are obtained from each wide-focused transmitted line. This shortens the acquisition time at the expense of introducing block artifacts. In this paper, we propose a data-driven learning-based approach to improve the MLA image quality. We train an end-to-end convolutional neural network on pairs of real ultrasound cardiac data, acquired through MLA and the corresponding single-line acquisition (SLA). The network achieves a significant improvement in image quality for both 5- and 7-line MLA resulting in a decorrelation measure similar to that of SLA while having the frame rate of MLA.}, author = {Senouf, Ortal and Vedula, Sanketh and Zurakhov, Grigoriy and Bronstein, Alexander and Zibulevsky, Michael and Michailovich, Oleg and Adam, Dan and Blondheim, David}, booktitle = {International Conference on Medical Image Computing and Computer Assisted Intervention}, isbn = {9783030009274}, issn = {1611-3349}, location = {Granada, Spain}, number = {Part 1}, pages = {126 -- 134}, publisher = {Springer Nature}, title = {{High frame-rate cardiac ultrasound imaging with deep learning}}, doi = {10.1007/978-3-030-00928-1_15}, volume = {11070}, year = {2018}, } @inproceedings{18284, abstract = {Frame rate is a crucial consideration in cardiac ultrasound imaging and 3D sonography. Several methods have been proposed in the medical ultrasound literature aiming at accelerating the image acquisition. In this paper, we consider one such method called multi-line transmission (MLT), in which several evenly separated focused beams are transmitted simultaneously. While MLT reduces the acquisition time, it comes at the expense of a heavy loss of contrast due to the interactions between the beams (cross-talk artifact). In this paper, we introduce a data-driven method to reduce the artifacts arising in MLT. To this end, we propose to train an end-to-end convolutional neural network consisting of correction layers followed by a constant apodization layer. The network is trained on pairs of raw data obtained through MLT and the corresponding single-line transmission (SLT) data. Experimental evaluation demonstrates significant improvement both in the visual image quality and in objective measures such as contrast ratio and contrast-to-noise ratio, while preserving resolution unlike traditional apodization-based methods. We show that the proposed method is able to generalize well across different patients and anatomies on real and phantom data.}, author = {Vedula, Sanketh and Senouf, Ortal and Zurakhov, Grigoriy and Bronstein, Alexander and Zibulevsky, Michael and Michailovich, Oleg and Adam, Dan and Gaitini, Diana}, booktitle = {First International Workshop, MLMIR 2018, Held in Conjunction with MICCAI 2018}, isbn = {9783030001285}, issn = {1611-3349}, location = {Granada, Spain}, pages = {147 -- 155}, publisher = {Springer Nature}, title = {{High quality ultrasonic multi-line transmission through deep learning}}, doi = {10.1007/978-3-030-00129-2_17}, volume = {11074}, year = {2018}, } @inproceedings{18285, abstract = {Single image depth estimation is achieved using computational imaging and Deep Learning (DL). Imaging with phase-mask is also modeled as a DL-layer, and the mask and DL parameters are jointly designed using labeled data.}, author = {Haim, Harel and Elmalem, Shay and Giryes, Raja and Bronstein, Alexander and Marom, Emanuel}, booktitle = {Imaging and Applied Optics 2018 (3D, AO, AIO, COSI, DH, IS, LACSEA, LS&C, MATH, pcAOP)}, isbn = {9781943580446}, location = {Orlando, FL, United States}, publisher = {OSA}, title = {{Deep learned phase mask for single image depth estimation and 3D scanning}}, doi = {10.1364/cosi.2018.cw3b.3}, volume = {Part F99-COSI 2018}, year = {2018}, } @inproceedings{183, abstract = {Fault-localization is considered to be a very tedious and time-consuming activity in the design of complex Cyber-Physical Systems (CPS). This laborious task essentially requires expert knowledge of the system in order to discover the cause of the fault. In this context, we propose a new procedure that AIDS designers in debugging Simulink/Stateflow hybrid system models, guided by Signal Temporal Logic (STL) specifications. The proposed method relies on three main ingredients: (1) a monitoring and a trace diagnostics procedure that checks whether a tested behavior satisfies or violates an STL specification, localizes time segments and interfaces variables contributing to the property violations; (2) a slicing procedure that maps these observable behavior segments to the internal states and transitions of the Simulink model; and (3) a spectrum-based fault-localization method that combines the previous analysis from multiple tests to identify the internal states and/or transitions that are the most likely to explain the fault. We demonstrate the applicability of our approach on two Simulink models from the automotive and the avionics domain.}, author = {Bartocci, Ezio and Ferrere, Thomas and Manjunath, Niveditha and Nickovic, Dejan}, location = {Porto, Portugal}, pages = {197 -- 206}, publisher = {Association for Computing Machinery}, title = {{Localizing faults in simulink/stateflow models with STL}}, doi = {10.1145/3178126.3178131}, year = {2018}, } @inproceedings{184, abstract = {We prove that for every d ≥ 2, deciding if a pure, d-dimensional, simplicial complex is shellable is NP-hard, hence NP-complete. This resolves a question raised, e.g., by Danaraj and Klee in 1978. Our reduction also yields that for every d ≥ 2 and k ≥ 0, deciding if a pure, d-dimensional, simplicial complex is k-decomposable is NP-hard. For d ≥ 3, both problems remain NP-hard when restricted to contractible pure d-dimensional complexes.}, author = {Goaoc, Xavier and Paták, Pavel and Patakova, Zuzana and Tancer, Martin and Wagner, Uli}, location = {Budapest, Hungary}, pages = {41:1 -- 41:16}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Shellability is NP-complete}}, doi = {10.4230/LIPIcs.SoCG.2018.41}, volume = {99}, year = {2018}, } @article{76, abstract = {Consider a fully-connected synchronous distributed system consisting of n nodes, where up to f nodes may be faulty and every node starts in an arbitrary initial state. In the synchronous C-counting problem, all nodes need to eventually agree on a counter that is increased by one modulo C in each round for given C>1. In the self-stabilising firing squad problem, the task is to eventually guarantee that all non-faulty nodes have simultaneous responses to external inputs: if a subset of the correct nodes receive an external “go” signal as input, then all correct nodes should agree on a round (in the not-too-distant future) in which to jointly output a “fire” signal. Moreover, no node should generate a “fire” signal without some correct node having previously received a “go” signal as input. We present a framework reducing both tasks to binary consensus at very small cost. For example, we obtain a deterministic algorithm for self-stabilising Byzantine firing squads with optimal resilience f<n/3, asymptotically optimal stabilisation and response time O(f), and message size O(log f). As our framework does not restrict the type of consensus routines used, we also obtain efficient randomised solutions.}, author = {Lenzen, Christoph and Rybicki, Joel}, journal = {Distributed Computing}, publisher = {Springer}, title = {{Near-optimal self-stabilising counting and firing squads}}, doi = {10.1007/s00446-018-0342-6}, year = {2018}, } @article{77, abstract = {Holes confined in quantum dots have gained considerable interest in the past few years due to their potential as spin qubits. Here we demonstrate two-axis control of a spin 3/2 qubit in natural Ge. The qubit is formed in a hut wire double quantum dot device. The Pauli spin blockade principle allowed us to demonstrate electric dipole spin resonance by applying a radio frequency electric field to one of the electrodes defining the double quantum dot. Coherent hole spin oscillations with Rabi frequencies reaching 140 MHz are demonstrated and dephasing times of 130 ns are measured. The reported results emphasize the potential of Ge as a platform for fast and electrically tunable hole spin qubit devices.}, author = {Watzinger, Hannes and Kukucka, Josip and Vukusic, Lada and Gao, Fei and Wang, Ting and Schäffler, Friedrich and Zhang, Jian and Katsaros, Georgios}, journal = {Nature Communications}, number = {3902 }, publisher = {Nature Publishing Group}, title = {{A germanium hole spin qubit}}, doi = {10.1038/s41467-018-06418-4}, volume = {9}, year = {2018}, } @article{7715, abstract = {Preference for mates with similar phenotypes; that is, assortative mating, is widely observed in humans1,2,3,4,5 and has evolutionary consequences6,7,8. Under Fisher's classical theory6, assortative mating is predicted to induce a signature in the genome at trait-associated loci that can be detected and quantified. Here, we develop and apply a method to quantify assortative mating on a specific trait by estimating the correlation (θ) between genetic predictors of the trait from single nucleotide polymorphisms on odd- versus even-numbered chromosomes. We show by theory and simulation that the effect of assortative mating can be quantified in the presence of population stratification. We applied this approach to 32 complex traits and diseases using single nucleotide polymorphism data from ~400,000 unrelated individuals of European ancestry. We found significant evidence of assortative mating for height (θ = 3.2%) and educational attainment (θ = 2.7%), both of which were consistent with theoretical predictions. Overall, our results imply that assortative mating involves multiple traits and affects the genomic architecture of loci that are associated with these traits, and that the consequence of mate choice can be detected from a random sample of genomes.}, author = {Yengo, Loic and Robinson, Matthew Richard and Keller, Matthew C. and Kemper, Kathryn E. and Yang, Yuanhao and Trzaskowski, Maciej and Gratten, Jacob and Turley, Patrick and Cesarini, David and Benjamin, Daniel J. and Wray, Naomi R. and Goddard, Michael E. and Yang, Jian and Visscher, Peter M.}, issn = {2397-3374}, journal = {Nature Human Behaviour}, number = {12}, pages = {948--954}, publisher = {Springer Nature}, title = {{Imprint of assortative mating on the human genome}}, doi = {10.1038/s41562-018-0476-3}, volume = {2}, year = {2018}, } @inproceedings{78, abstract = {We provide a procedure for detecting the sub-segments of an incrementally observed Boolean signal ω that match a given temporal pattern ϕ. As a pattern specification language, we use timed regular expressions, a formalism well-suited for expressing properties of concurrent asynchronous behaviors embedded in metric time. We construct a timed automaton accepting the timed language denoted by ϕ and modify it slightly for the purpose of matching. We then apply zone-based reachability computation to this automaton while it reads ω, and retrieve all the matching segments from the results. Since the procedure is automaton based, it can be applied to patterns specified by other formalisms such as timed temporal logics reducible to timed automata or directly encoded as timed automata. The procedure has been implemented and its performance on synthetic examples is demonstrated.}, author = {Bakhirkin, Alexey and Ferrere, Thomas and Nickovic, Dejan and Maler, Oded and Asarin, Eugene}, isbn = {978-3-030-00150-6}, location = {Bejing, China}, pages = {215 -- 232}, publisher = {Springer}, title = {{Online timed pattern matching using automata}}, doi = {10.1007/978-3-030-00151-3_13}, volume = {11022}, year = {2018}, }