@article{7009, abstract = {Cell migration is essential for physiological processes as diverse as development, immune defence and wound healing. It is also a hallmark of cancer malignancy. Thousands of publications have elucidated detailed molecular and biophysical mechanisms of cultured cells migrating on flat, 2D substrates of glass and plastic. However, much less is known about how cells successfully navigate the complex 3D environments of living tissues. In these more complex, native environments, cells use multiple modes of migration, including mesenchymal, amoeboid, lobopodial and collective, and these are governed by the local extracellular microenvironment, specific modalities of Rho GTPase signalling and non- muscle myosin contractility. Migration through 3D environments is challenging because it requires the cell to squeeze through complex or dense extracellular structures. Doing so requires specific cellular adaptations to mechanical features of the extracellular matrix (ECM) or its remodelling. In addition, besides navigating through diverse ECM environments and overcoming extracellular barriers, cells often interact with neighbouring cells and tissues through physical and signalling interactions. Accordingly, cells need to call on an impressively wide diversity of mechanisms to meet these challenges. This Review examines how cells use both classical and novel mechanisms of locomotion as they traverse challenging 3D matrices and cellular environments. It focuses on principles rather than details of migratory mechanisms and draws comparisons between 1D, 2D and 3D migration.}, author = {Yamada, KM and Sixt, Michael K}, issn = {1471-0080}, journal = {Nature Reviews Molecular Cell Biology}, number = {12}, pages = {738–752}, publisher = {Springer Nature}, title = {{Mechanisms of 3D cell migration}}, doi = {10.1038/s41580-019-0172-9}, volume = {20}, year = {2019}, } @inproceedings{7010, abstract = {Numerous biophysical questions require the quantification of short-range interactions between (functionalized) surfaces and synthetic or biological objects such as cells. Here, we present an original, custom built setup for reflection interference contrast microscopy that can assess distances between a substrate and a flowing object at high speed with nanometric accuracy. We demonstrate its use to decipher the complex biochemical and mechanical interplay regulating blood cell homing at the vessel wall in the microcirculation using an in vitro approach. We show that in the absence of specific biochemical interactions, flowing cells are repelled from the soft layer lining the vessel wall, contributing to red blood cell repulsion in vivo. In contrast, this so-called glycocalyx stabilizes rolling of cells under flow in the presence of a specific receptor naturally present on activated leucocytes and a number of cancer cell lines.}, author = {Davies, Heather S. and Baranova, Natalia S. and El Amri, Nouha and Coche-Guérente, Liliane and Verdier, Claude and Bureau, Lionel and Richter, Ralf P. and Débarre, Delphine}, booktitle = {Advances in Microscopic Imaging II}, isbn = {9781510628458}, issn = {1605-7422}, location = {Munich, Germany}, publisher = {SPIE}, title = {{Blood cell-vessel wall interactions probed by reflection interference contrast microscopy}}, doi = {10.1117/12.2527058}, volume = {11076}, year = {2019}, } @article{7013, abstract = {Chains of superconducting circuit devices provide a natural platform for studies of synthetic bosonic quantum matter. Motivated by the recent experimental progress in realizing disordered and interacting chains of superconducting transmon devices, we study the bosonic many-body localization phase transition using the methods of exact diagonalization as well as matrix product state dynamics. We estimate the location of transition separating the ergodic and the many-body localized phases as a function of the disorder strength and the many-body on-site interaction strength. The main difference between the bosonic model realized by superconducting circuits and similar fermionic model is that the effect of the on-site interaction is stronger due to the possibility of multiple excitations occupying the same site. The phase transition is found to be robust upon including longer-range hopping and interaction terms present in the experiments. Furthermore, we calculate experimentally relevant local observables and show that their temporal fluctuations can be used to distinguish between the dynamics of Anderson insulator, many-body localization, and delocalized phases. While we consider unitary dynamics, neglecting the effects of dissipation, decoherence, and measurement back action, the timescales on which the dynamics is unitary are sufficient for observation of characteristic dynamics in the many-body localized phase. Moreover, the experimentally available disorder strength and interactions allow for tuning the many-body localization phase transition, thus making the arrays of superconducting circuit devices a promising platform for exploring localization physics and phase transition.}, author = {Orell, Tuure and Michailidis, Alexios and Serbyn, Maksym and Silveri, Matti}, issn = {2469-9969}, journal = {Physical Review B}, number = {13}, publisher = {American Physical Society}, title = {{Probing the many-body localization phase transition with superconducting circuits}}, doi = {10.1103/physrevb.100.134504}, volume = {100}, year = {2019}, } @article{7014, abstract = {We study the problem of developing efficient approaches for proving worst-case bounds of non-deterministic recursive programs. Ranking functions are sound and complete for proving termination and worst-case bounds of nonrecursive programs. First, we apply ranking functions to recursion, resulting in measure functions. We show that measure functions provide a sound and complete approach to prove worst-case bounds of non-deterministic recursive programs. Our second contribution is the synthesis of measure functions in nonpolynomial forms. We show that non-polynomial measure functions with logarithm and exponentiation can be synthesized through abstraction of logarithmic or exponentiation terms, Farkas' Lemma, and Handelman's Theorem using linear programming. While previous methods obtain worst-case polynomial bounds, our approach can synthesize bounds of the form $\mathcal{O}(n\log n)$ as well as $\mathcal{O}(n^r)$ where $r$ is not an integer. We present experimental results to demonstrate that our approach can obtain efficiently worst-case bounds of classical recursive algorithms such as (i) Merge-Sort, the divide-and-conquer algorithm for the Closest-Pair problem, where we obtain $\mathcal{O}(n \log n)$ worst-case bound, and (ii) Karatsuba's algorithm for polynomial multiplication and Strassen's algorithm for matrix multiplication, where we obtain $\mathcal{O}(n^r)$ bound such that $r$ is not an integer and close to the best-known bounds for the respective algorithms.}, author = {Chatterjee, Krishnendu and Fu, Hongfei and Goharshady, Amir Kafshdar}, journal = {ACM Transactions on Programming Languages and Systems}, number = {4}, publisher = {ACM}, title = {{Non-polynomial worst-case analysis of recursive programs}}, doi = {10.1145/3339984}, volume = {41}, year = {2019}, } @article{7015, abstract = {We modify the "floating crystal" trial state for the classical homogeneous electron gas (also known as jellium), in order to suppress the boundary charge fluctuations that are known to lead to a macroscopic increase of the energy. The argument is to melt a thin layer of the crystal close to the boundary and consequently replace it by an incompressible fluid. With the aid of this trial state we show that three different definitions of the ground-state energy of jellium coincide. In the first point of view the electrons are placed in a neutralizing uniform background. In the second definition there is no background but the electrons are submitted to the constraint that their density is constant, as is appropriate in density functional theory. Finally, in the third system each electron interacts with a periodic image of itself; that is, periodic boundary conditions are imposed on the interaction potential.}, author = {Lewin, Mathieu and Lieb, Elliott H. and Seiringer, Robert}, issn = {2469-9969}, journal = {Physical Review B}, number = {3}, publisher = {American Physical Society}, title = {{Floating Wigner crystal with no boundary charge fluctuations}}, doi = {10.1103/physrevb.100.035127}, volume = {100}, year = {2019}, } @misc{7016, abstract = {Organisms cope with change by employing transcriptional regulators. However, when faced with rare environments, the evolution of transcriptional regulators and their promoters may be too slow. We ask whether the intrinsic instability of gene duplication and amplification provides a generic alternative to canonical gene regulation. By real-time monitoring of gene copy number mutations in E. coli, we show that gene duplications and amplifications enable adaptation to fluctuating environments by rapidly generating copy number, and hence expression level, polymorphism. This ‘amplification-mediated gene expression tuning’ occurs on timescales similar to canonical gene regulation and can deal with rapid environmental changes. Mathematical modeling shows that amplifications also tune gene expression in stochastic environments where transcription factor-based schemes are hard to evolve or maintain. The fleeting nature of gene amplifications gives rise to a generic population-level mechanism that relies on genetic heterogeneity to rapidly tune expression of any gene, without leaving any genomic signature.}, author = {Tomanek, Isabella}, keywords = {Escherichia coli, gene amplification, galactose, DOG, experimental evolution, Illumina sequence data, FACS data, microfluidics data}, publisher = {Institute of Science and Technology Austria}, title = {{Data for the paper "Gene amplification as a form of population-level gene expression regulation"}}, doi = {10.15479/AT:ISTA:7016}, year = {2019}, } @article{7026, abstract = {Effective design of combination therapies requires understanding the changes in cell physiology that result from drug interactions. Here, we show that the genome-wide transcriptional response to combinations of two drugs, measured at a rigorously controlled growth rate, can predict higher-order antagonism with a third drug in Saccharomyces cerevisiae. Using isogrowth profiling, over 90% of the variation in cellular response can be decomposed into three principal components (PCs) that have clear biological interpretations. We demonstrate that the third PC captures emergent transcriptional programs that are dependent on both drugs and can predict antagonism with a third drug targeting the emergent pathway. We further show that emergent gene expression patterns are most pronounced at a drug ratio where the drug interaction is strongest, providing a guideline for future measurements. Our results provide a readily applicable recipe for uncovering emergent responses in other systems and for higher-order drug combinations. A record of this paper’s transparent peer review process is included in the Supplemental Information.}, author = {Lukacisin, Martin and Bollenbach, Tobias}, issn = {2405-4712}, journal = {Cell Systems}, number = {5}, pages = {423--433.e1--e3}, publisher = {Cell Press}, title = {{Emergent gene expression responses to drug combinations predict higher-order drug interactions}}, doi = {10.1016/j.cels.2019.10.004}, volume = {9}, year = {2019}, } @inproceedings{7032, abstract = {Optical frequency combs (OFCs) are light sources whose spectra consists of equally spaced frequency lines in the optical domain [1]. They have great potential for improving high-capacity data transfer, all-optical atomic clocks, spectroscopy, and high-precision measurements [2].}, author = {Rueda Sanchez, Alfredo R and Sedlmeir, Florian and Leuchs, Gerd and Kuamri, Madhuri and Schwefel, Harald G. L.}, booktitle = {2019 Conference on Lasers and Electro-Optics Europe & European Quantum Electronics Conference}, isbn = {9781728104690}, location = {Munich, Germany}, publisher = {IEEE}, title = {{Electro-optic frequency comb generation in lithium niobate whispering gallery mode resonators}}, doi = {10.1109/cleoe-eqec.2019.8873300}, year = {2019}, } @article{7034, abstract = {We find a graph of genus 5 and its drawing on the orientable surface of genus 4 with every pair of independent edges crossing an even number of times. This shows that the strong Hanani–Tutte theorem cannot be extended to the orientable surface of genus 4. As a base step in the construction we use a counterexample to an extension of the unified Hanani–Tutte theorem on the torus.}, author = {Fulek, Radoslav and Kynčl, Jan}, issn = {1439-6912}, journal = {Combinatorica}, number = {6}, pages = {1267--1279}, publisher = {Springer Nature}, title = {{Counterexample to an extension of the Hanani-Tutte theorem on the surface of genus 4}}, doi = {10.1007/s00493-019-3905-7}, volume = {39}, year = {2019}, } @inproceedings{7035, abstract = {The aim of this short note is to expound one particular issue that was discussed during the talk [10] given at the symposium ”Researches on isometries as preserver problems and related topics” at Kyoto RIMS. That is, the role of Dirac masses by describing the isometry group of various metric spaces of probability measures. This article is of survey character, and it does not contain any essentially new results.From an isometric point of view, in some cases, metric spaces of measures are similar to C(K)-type function spaces. Similarity means here that their isometries are driven by some nice transformations of the underlying space. Of course, it depends on the particular choice of the metric how nice these transformations should be. Sometimes, as we will see, being a homeomorphism is enough to generate an isometry. But sometimes we need more: the transformation must preserve the underlying distance as well. Statements claiming that isometries in questions are necessarily induced by homeomorphisms are called Banach-Stone-type results, while results asserting that the underlying transformation is necessarily an isometry are termed as isometric rigidity results.As Dirac masses can be considered as building bricks of the set of all Borel measures, a natural question arises:Is it enough to understand how an isometry acts on the set of Dirac masses? Does this action extend uniquely to all measures?In what follows, we will thoroughly investigate this question.}, author = {Geher, Gyorgy Pal and Titkos, Tamas and Virosztek, Daniel}, booktitle = {Kyoto RIMS Kôkyûroku}, location = {Kyoto, Japan}, pages = {34--41}, publisher = {Research Institute for Mathematical Sciences, Kyoto University}, title = {{Dirac masses and isometric rigidity}}, volume = {2125}, year = {2019}, } @article{7093, abstract = {In graph theory, as well as in 3-manifold topology, there exist several width-type parameters to describe how "simple" or "thin" a given graph or 3-manifold is. These parameters, such as pathwidth or treewidth for graphs, or the concept of thin position for 3-manifolds, play an important role when studying algorithmic problems; in particular, there is a variety of problems in computational 3-manifold topology - some of them known to be computationally hard in general - that become solvable in polynomial time as soon as the dual graph of the input triangulation has bounded treewidth. In view of these algorithmic results, it is natural to ask whether every 3-manifold admits a triangulation of bounded treewidth. We show that this is not the case, i.e., that there exists an infinite family of closed 3-manifolds not admitting triangulations of bounded pathwidth or treewidth (the latter implies the former, but we present two separate proofs). We derive these results from work of Agol, of Scharlemann and Thompson, and of Scharlemann, Schultens and Saito by exhibiting explicit connections between the topology of a 3-manifold M on the one hand and width-type parameters of the dual graphs of triangulations of M on the other hand, answering a question that had been raised repeatedly by researchers in computational 3-manifold topology. In particular, we show that if a closed, orientable, irreducible, non-Haken 3-manifold M has a triangulation of treewidth (resp. pathwidth) k then the Heegaard genus of M is at most 18(k+1) (resp. 4(3k+1)).}, author = {Huszár, Kristóf and Spreer, Jonathan and Wagner, Uli}, issn = {1920-180X}, journal = {Journal of Computational Geometry}, number = {2}, pages = {70–98}, publisher = {Computational Geometry Laborartoy}, title = {{On the treewidth of triangulated 3-manifolds}}, doi = {10.20382/JOGC.V10I2A5}, volume = {10}, year = {2019}, } @article{7095, abstract = {BAX, a member of the BCL2 gene family, controls the committed step of the intrinsic apoptotic program. Mitochondrial fragmentation is a commonly observed feature of apoptosis, which occurs through the process of mitochondrial fission. BAX has consistently been associated with mitochondrial fission, yet how BAX participates in the process of mitochondrial fragmentation during apoptosis remains to be tested. Time-lapse imaging of BAX recruitment and mitochondrial fragmentation demonstrates that rapid mitochondrial fragmentation during apoptosis occurs after the complete recruitment of BAX to the mitochondrial outer membrane (MOM). The requirement of a fully functioning BAX protein for the fission process was demonstrated further in BAX/BAK-deficient HCT116 cells expressing a P168A mutant of BAX. The mutant performed fusion to restore the mitochondrial network. but was not demonstrably recruited to the MOM after apoptosis induction. Under these conditions, mitochondrial fragmentation was blocked. Additionally, we show that loss of the fission protein, dynamin-like protein 1 (DRP1), does not temporally affect the initiation time or rate of BAX recruitment, but does reduce the final level of BAX recruited to the MOM during the late phase of BAX recruitment. These correlative observations suggest a model where late-stage BAX oligomers play a functional part of the mitochondrial fragmentation machinery in apoptotic cells.}, author = {Maes, Margaret E and Grosser, J. A. and Fehrman, R. L. and Schlamp, C. L. and Nickells, R. W.}, issn = {2045-2322}, journal = {Scientific Reports}, publisher = {Springer Nature}, title = {{Completion of BAX recruitment correlates with mitochondrial fission during apoptosis}}, doi = {10.1038/s41598-019-53049-w}, volume = {9}, year = {2019}, } @article{7097, abstract = {Early endosomes, also called sorting endosomes, are known to mature into late endosomesvia the Rab5-mediated endolysosomal trafficking pathway. Thus, early endosome existence isthought to be maintained by the continual fusion of transport vesicles from the plasmamembrane and thetrans-Golgi network (TGN). Here we show instead that endocytosis isdispensable and post-Golgi vesicle transport is crucial for the formation of endosomes andthe subsequent endolysosomal traffic regulated by yeast Rab5 Vps21p. Fittingly, all threeproteins required for endosomal nucleotide exchange on Vps21p arefirst recruited to theTGN before transport to the endosome, namely the GEF Vps9p and the epsin-relatedadaptors Ent3/5p. The TGN recruitment of these components is distinctly controlled, withVps9p appearing to require the Arf1p GTPase, and the Rab11s, Ypt31p/32p. These resultsprovide a different view of endosome formation and identify the TGN as a critical location forregulating progress through the endolysosomal trafficking pathway.}, author = {Nagano, Makoto and Toshima, Junko Y. and Siekhaus, Daria E and Toshima, Jiro}, issn = {2399-3642}, journal = {Communications Biology}, number = {1}, publisher = {Springer Nature}, title = {{Rab5-mediated endosome formation is regulated at the trans-Golgi network}}, doi = {10.1038/s42003-019-0670-5}, volume = {2}, year = {2019}, } @article{7099, author = {Kasugai, Yu and Vogel, Elisabeth and Hörtnagl, Heide and Schönherr, Sabine and Paradiso, Enrica and Hauschild, Markus and Göbel, Georg and Milenkovic, Ivan and Peterschmitt, Yvan and Tasan, Ramon and Sperk, Günther and Shigemoto, Ryuichi and Sieghart, Werner and Singewald, Nicolas and Lüthi, Andreas and Ferraguti, Francesco}, issn = {0896-6273}, journal = {Neuron}, number = {4}, pages = {781--794.e4}, publisher = {Elsevier}, title = {{Structural and functional remodeling of amygdala GABAergic synapses in associative fear learning}}, doi = {10.1016/j.neuron.2019.08.013}, volume = {104}, year = {2019}, } @article{7100, abstract = {We present microscopic derivations of the defocusing two-dimensional cubic nonlinear Schrödinger equation and the Gross–Pitaevskii equation starting froman interacting N-particle system of bosons. We consider the interaction potential to be given either by Wβ(x)=N−1+2βW(Nβx), for any β>0, or to be given by VN(x)=e2NV(eNx), for some spherical symmetric, nonnegative and compactly supported W,V∈L∞(R2,R). In both cases we prove the convergence of the reduced density corresponding to the exact time evolution to the projector onto the solution of the corresponding nonlinear Schrödinger equation in trace norm. For the latter potential VN we show that it is crucial to take the microscopic structure of the condensate into account in order to obtain the correct dynamics.}, author = {Jeblick, Maximilian and Leopold, Nikolai K and Pickl, Peter}, issn = {1432-0916}, journal = {Communications in Mathematical Physics}, number = {1}, pages = {1--69}, publisher = {Springer Nature}, title = {{Derivation of the time dependent Gross–Pitaevskii equation in two dimensions}}, doi = {10.1007/s00220-019-03599-x}, volume = {372}, year = {2019}, } @article{7103, abstract = {Origin and functions of intermittent transitions among sleep stages, including short awakenings and arousals, constitute a challenge to the current homeostatic framework for sleep regulation, focusing on factors modulating sleep over large time scales. Here we propose that the complex micro-architecture characterizing the sleep-wake cycle results from an underlying non-equilibrium critical dynamics, bridging collective behaviors across spatio-temporal scales. We investigate θ and δ wave dynamics in control rats and in rats with lesions of sleep-promoting neurons in the parafacial zone. We demonstrate that intermittent bursts in θ and δ rhythms exhibit a complex temporal organization, with long-range power-law correlations and a robust duality of power law (θ-bursts, active phase) and exponential-like (δ-bursts, quiescent phase) duration distributions, typical features of non-equilibrium systems self-organizing at criticality. Crucially, such temporal organization relates to anti-correlated coupling between θ- and δ-bursts, and is independent of the dominant physiologic state and lesions, a solid indication of a basic principle in sleep dynamics.}, author = {Wang, Jilin W. J. L. and Lombardi, Fabrizio and Zhang, Xiyun and Anaclet, Christelle and Ivanov, Plamen Ch.}, issn = {1553-7358}, journal = {PLoS Computational Biology}, number = {11}, publisher = {Public Library of Science}, title = {{Non-equilibrium critical dynamics of bursts in θ and δ rhythms as fundamental characteristic of sleep and wake micro-architecture}}, doi = {10.1371/journal.pcbi.1007268}, volume = {15}, year = {2019}, } @article{7105, abstract = {Cell migration is hypothesized to involve a cycle of behaviours beginning with leading edge extension. However, recent evidence suggests that the leading edge may be dispensable for migration, raising the question of what actually controls cell directionality. Here, we exploit the embryonic migration of Drosophila macrophages to bridge the different temporal scales of the behaviours controlling motility. This approach reveals that edge fluctuations during random motility are not persistent and are weakly correlated with motion. In contrast, flow of the actin network behind the leading edge is highly persistent. Quantification of actin flow structure during migration reveals a stable organization and asymmetry in the cell-wide flowfield that strongly correlates with cell directionality. This organization is regulated by a gradient of actin network compression and destruction, which is controlled by myosin contraction and cofilin-mediated disassembly. It is this stable actin-flow polarity, which integrates rapid fluctuations of the leading edge, that controls inherent cellular persistence.}, author = {Yolland, Lawrence and Burki, Mubarik and Marcotti, Stefania and Luchici, Andrei and Kenny, Fiona N. and Davis, John Robert and Serna-Morales, Eduardo and Müller, Jan and Sixt, Michael K and Davidson, Andrew and Wood, Will and Schumacher, Linus J. and Endres, Robert G. and Miodownik, Mark and Stramer, Brian M.}, issn = {1476-4679}, journal = {Nature Cell Biology}, number = {11}, pages = {1370--1381}, publisher = {Springer Nature}, title = {{Persistent and polarized global actin flow is essential for directionality during cell migration}}, doi = {10.1038/s41556-019-0411-5}, volume = {21}, year = {2019}, } @article{7106, abstract = {PIN-FORMED (PIN) transporters mediate directional, intercellular movement of the phytohormone auxin in land plants. To elucidate the evolutionary origins of this developmentally crucial mechanism, we analysed the single PIN homologue of a simple green alga Klebsormidium flaccidum. KfPIN functions as a plasma membrane-localized auxin exporter in land plants and heterologous models. While its role in algae remains unclear, PIN-driven auxin export is probably an ancient and conserved trait within streptophytes.}, author = {Skokan, Roman and Medvecká, Eva and Viaene, Tom and Vosolsobě, Stanislav and Zwiewka, Marta and Müller, Karel and Skůpa, Petr and Karady, Michal and Zhang, Yuzhou and Janacek, Dorina P. and Hammes, Ulrich Z. and Ljung, Karin and Nodzyński, Tomasz and Petrášek, Jan and Friml, Jiří}, issn = {2055-0278}, journal = {Nature Plants}, number = {11}, pages = {1114--1119}, publisher = {Springer Nature}, title = {{PIN-driven auxin transport emerged early in streptophyte evolution}}, doi = {10.1038/s41477-019-0542-5}, volume = {5}, year = {2019}, } @article{7108, 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. Another simple corollary of our result is that it is NP-hard to decide whether a given poset is CL-shellable.}, author = {Goaoc, Xavier and Patak, Pavel and Patakova, Zuzana and Tancer, Martin and Wagner, Uli}, issn = {0004-5411}, journal = {Journal of the ACM}, number = {3}, publisher = {ACM}, title = {{Shellability is NP-complete}}, doi = {10.1145/3314024}, volume = {66}, year = {2019}, } @article{7109, abstract = {We show how to construct temporal testers for the logic MITL, a prominent linear-time logic for real-time systems. A temporal tester is a transducer that inputs a signal holding the Boolean value of atomic propositions and outputs the truth value of a formula along time. Here we consider testers over continuous-time Boolean signals that use clock variables to enforce duration constraints, as in timed automata. We first rewrite the MITL formula into a “simple” formula using a limited set of temporal modalities. We then build testers for these specific modalities and show how to compose testers for simple formulae into complex ones. Temporal testers can be turned into acceptors, yielding a compositional translation from MITL to timed automata. This construction is much simpler than previously known and remains asymptotically optimal. It supports both past and future operators and can easily be extended.}, author = {Ferrere, Thomas and Maler, Oded and Ničković, Dejan and Pnueli, Amir}, issn = {0004-5411}, journal = {Journal of the ACM}, number = {3}, publisher = {ACM}, title = {{From real-time logic to timed automata}}, doi = {10.1145/3286976}, volume = {66}, year = {2019}, }