@article{13049, abstract = {We propose a computational design approach for covering a surface with individually addressable RGB LEDs, effectively forming a low-resolution surface screen. To achieve a low-cost and scalable approach, we propose creating designs from flat PCB panels bent in-place along the surface of a 3D printed core. Working with standard rigid PCBs enables the use of established PCB manufacturing services, allowing the fabrication of designs with several hundred LEDs. Our approach optimizes the PCB geometry for folding, and then jointly optimizes the LED packing, circuit and routing, solving a challenging layout problem under strict manufacturing requirements. Unlike paper, PCBs cannot bend beyond a certain point without breaking. Therefore, we introduce parametric cut patterns acting as hinges, designed to allow bending while remaining compact. To tackle the joint optimization of placement, circuit and routing, we propose a specialized algorithm that splits the global problem into one sub-problem per triangle, which is then individually solved. Our technique generates PCB blueprints in a completely automated way. After being fabricated by a PCB manufacturing service, the boards are bent and glued by the user onto the 3D printed support. We demonstrate our technique on a range of physical models and virtual examples, creating intricate surface light patterns from hundreds of LEDs.}, author = {Freire, Marco and Bhargava, Manas and Schreck, Camille and Hugron, Pierre-Alexandre and Bickel, Bernd and Lefebvre, Sylvain}, issn = {1557-7368}, journal = {Transactions on Graphics}, keywords = {PCB design and layout, Mesh geometry models}, location = {Los Angeles, CA, United States}, number = {4}, publisher = {Association for Computing Machinery}, title = {{PCBend: Light up your 3D shapes with foldable circuit boards}}, doi = {10.1145/3592411}, volume = {42}, year = {2023}, } @inproceedings{13053, abstract = {Deep neural networks (DNNs) often have to be compressed, via pruning and/or quantization, before they can be deployed in practical settings. In this work we propose a new compression-aware minimizer dubbed CrAM that modifies the optimization step in a principled way, in order to produce models whose local loss behavior is stable under compression operations such as pruning. Thus, dense models trained via CrAM should be compressible post-training, in a single step, without significant accuracy loss. Experimental results on standard benchmarks, such as residual networks for ImageNet classification and BERT models for language modelling, show that CrAM produces dense models that can be more accurate than the standard SGD/Adam-based baselines, but which are stable under weight pruning: specifically, we can prune models in one-shot to 70-80% sparsity with almost no accuracy loss, and to 90% with reasonable (∼1%) accuracy loss, which is competitive with gradual compression methods. Additionally, CrAM can produce sparse models which perform well for transfer learning, and it also works for semi-structured 2:4 pruning patterns supported by GPU hardware. The code for reproducing the results is available at this https URL .}, author = {Peste, Elena-Alexandra and Vladu, Adrian and Kurtic, Eldar and Lampert, Christoph and Alistarh, Dan-Adrian}, booktitle = {11th International Conference on Learning Representations }, location = {Kigali, Rwanda }, title = {{CrAM: A Compression-Aware Minimizer}}, year = {2023}, } @phdthesis{13074, abstract = {Deep learning has become an integral part of a large number of important applications, and many of the recent breakthroughs have been enabled by the ability to train very large models, capable to capture complex patterns and relationships from the data. At the same time, the massive sizes of modern deep learning models have made their deployment to smaller devices more challenging; this is particularly important, as in many applications the users rely on accurate deep learning predictions, but they only have access to devices with limited memory and compute power. One solution to this problem is to prune neural networks, by setting as many of their parameters as possible to zero, to obtain accurate sparse models with lower memory footprint. Despite the great research progress in obtaining sparse models that preserve accuracy, while satisfying memory and computational constraints, there are still many challenges associated with efficiently training sparse models, as well as understanding their generalization properties. The focus of this thesis is to investigate how the training process of sparse models can be made more efficient, and to understand the differences between sparse and dense models in terms of how well they can generalize to changes in the data distribution. We first study a method for co-training sparse and dense models, at a lower cost compared to regular training. With our method we can obtain very accurate sparse networks, and dense models that can recover the baseline accuracy. Furthermore, we are able to more easily analyze the differences, at prediction level, between the sparse-dense model pairs. Next, we investigate the generalization properties of sparse neural networks in more detail, by studying how well different sparse models trained on a larger task can adapt to smaller, more specialized tasks, in a transfer learning scenario. Our analysis across multiple pruning methods and sparsity levels reveals that sparse models provide features that can transfer similarly to or better than the dense baseline. However, the choice of the pruning method plays an important role, and can influence the results when the features are fixed (linear finetuning), or when they are allowed to adapt to the new task (full finetuning). Using sparse models with fixed masks for finetuning on new tasks has an important practical advantage, as it enables training neural networks on smaller devices. However, one drawback of current pruning methods is that the entire training cycle has to be repeated to obtain the initial sparse model, for every sparsity target; in consequence, the entire training process is costly and also multiple models need to be stored. In the last part of the thesis we propose a method that can train accurate dense models that are compressible in a single step, to multiple sparsity levels, without additional finetuning. Our method results in sparse models that can be competitive with existing pruning methods, and which can also successfully generalize to new tasks.}, author = {Peste, Elena-Alexandra}, issn = {2663-337X}, pages = {147}, publisher = {Institute of Science and Technology Austria}, title = {{Efficiency and generalization of sparse neural networks}}, doi = {10.15479/at:ista:13074}, year = {2023}, } @phdthesis{13081, abstract = {During development, tissues undergo changes in size and shape to form functional organs. Distinct cellular processes such as cell division and cell rearrangements underlie tissue morphogenesis. Yet how the distinct processes are controlled and coordinated, and how they contribute to morphogenesis is poorly understood. In our study, we addressed these questions using the developing mouse neural tube. This epithelial organ transforms from a flat epithelial sheet to an epithelial tube while increasing in size and undergoing morpho-gen-mediated patterning. The extent and mechanism of neural progenitor rearrangement within the developing mouse neuroepithelium is unknown. To investigate this, we per-formed high resolution lineage tracing analysis to quantify the extent of epithelial rear-rangement at different stages of neural tube development. We quantitatively described the relationship between apical cell size with cell cycle dependent interkinetic nuclear migra-tions (IKNM) and performed high cellular resolution live imaging of the neuroepithelium to study the dynamics of junctional remodeling. Furthermore, developed a vertex model of the neuroepithelium to investigate the quantitative contribution of cell proliferation, cell differentiation and mechanical properties to the epithelial rearrangement dynamics and validated the model predictions through functional experiments. Our analysis revealed that at early developmental stages, the apical cell area kinetics driven by IKNM induce high lev-els of cell rearrangements in a regime of high junctional tension and contractility. After E9.5, there is a sharp decline in the extent of cell rearrangements, suggesting that the epi-thelium transitions from a fluid-like to a solid-like state. We found that this transition is regulated by the growth rate of the tissue, rather than by changes in cell-cell adhesion and contractile forces. Overall, our study provides a quantitative description of the relationship between tissue growth, cell cycle dynamics, epithelia rearrangements and the emergent tissue material properties, and novel insights on how epithelial cell dynamics influences tissue morphogenesis.}, author = {Bocanegra, Laura}, issn = {2663 - 337X}, pages = {93}, publisher = {Institute of Science and Technology Austria}, title = {{Epithelial dynamics during mouse neural tube development}}, doi = {10.15479/at:ista:13081}, year = {2023}, } @phdthesis{13107, abstract = {Within the human body, the brain exhibits the highest rate of energy consumption amongst all organs, with the majority of generated ATP being utilized to sustain neuronal activity. Therefore, the metabolism of the mature cerebral cortex is geared towards preserving metabolic homeostasis whilst generating significant amounts of energy. This requires a precise interplay between diverse metabolic pathways, spanning from a tissue-wide scale to the level of individual neurons. Disturbances to this delicate metabolic equilibrium, such as those resulting from maternal malnutrition or mutations affecting metabolic enzymes, often result in neuropathological variants of neurodevelopment. For instance, mutations in SLC7A5, a transporter of metabolically essential large neutral amino acids (LNAAs), have been associated with autism and microcephaly. However, despite recent progress in the field, the extent of metabolic restructuring that occurs within the developing brain and the corresponding alterations in nutrient demands during various critical periods remain largely unknown. To investigate this, we performed metabolomic profiling of the murine cerebral cortex to characterize the metabolic state of the forebrain at different developmental stages. We found that the developing cortex undergoes substantial metabolic reprogramming, with specific sets of metabolites displaying stage-specific changes. According to our observations, we determined a distinct temporal period in postnatal development during which the cortex displays heightened reliance on LNAAs. Hence, using a conditional knock-out mouse model, we deleted Slc7a5 in neural cells, allowing us to monitor the impact of a perturbed neuronal metabolic state across multiple developmental stages of corticogenesis. We found that manipulating the levels of essential LNAAs in cortical neurons in vivo affects one particular perinatal developmental period critical for cortical network refinement. Abnormally low intracellular LNAA levels result in cell-autonomous alterations in neuronal lipid metabolism, excitability, and survival during this particular time window. Although most of the effects of Slc7a5 deletion on neuronal physiology are transient, derailment of these processes during this brief but crucial window leads to long-term circuit dysfunction in mice. In conclusion, out data indicate that the cerebral cortex undergoes significant metabolic reorganization during development. This process involves the intricate integration of multiple metabolic pathways to ensure optimal neuronal function throughout different developmental stages. Our findings offer a paradigm for understanding how neurons synchronize the expression of nutrient-related genes with their activity to allow proper brain maturation. Further, our results demonstrate that disruptions in these precisely calibrated metabolic processes during critical periods of brain development may result in neuropathological outcomes in mice and in humans.}, author = {Knaus, Lisa}, issn = {2663 - 337X}, pages = {147}, publisher = {Institute of Science and Technology Austria}, title = {{The metabolism of the developing brain : How large neutral amino acids modulate perinatal neuronal excitability and survival}}, doi = {10.15479/at:ista:13107}, year = {2023}, } @inproceedings{13120, abstract = {We formalized general (i.e., type-0) grammars using the Lean 3 proof assistant. We defined basic notions of rewrite rules and of words derived by a grammar, and used grammars to show closure of the class of type-0 languages under four operations: union, reversal, concatenation, and the Kleene star. The literature mostly focuses on Turing machine arguments, which are possibly more difficult to formalize. For the Kleene star, we could not follow the literature and came up with our own grammar-based construction.}, author = {Dvorak, Martin and Blanchette, Jasmin}, booktitle = {14th International Conference on Interactive Theorem Proving}, isbn = {9783959772846}, issn = {1868-8969}, location = {Bialystok, Poland}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Closure properties of general grammars - formally verified}}, doi = {10.4230/LIPIcs.ITP.2023.15}, volume = {268}, year = {2023}, } @article{13128, abstract = {Given A⊆GL2(Fq), we prove that there exist disjoint subsets B,C⊆A such that A=B⊔C and their additive and multiplicative energies satisfying max{E+(B),E×(C)}≪|A|3/M(|A|), where M(|A|)=min{q4/3/|A|1/3(log|A|)2/3,|A|4/5/q13/5(log|A|)27/10}. We also study some related questions on moderate expanders over matrix rings, namely, for A,B,C⊆GL2(Fq), we have |AB+C|, |(A+B)C|≫q4, whenever |A||B||C|≫q10+1/2. These improve earlier results due to Karabulut, Koh, Pham, Shen, and Vinh ([2019], Expanding phenomena over matrix rings, ForumMath., 31, 951–970). }, author = {Mohammadi, Ali and Pham, Thang and Wang, Yiting}, issn = {1496-4287}, journal = {Canadian Mathematical Bulletin}, number = {4}, pages = {1280--1295}, publisher = {Cambridge University Press}, title = {{An energy decomposition theorem for matrices and related questions}}, doi = {10.4153/S000843952300036X}, volume = {66}, year = {2023}, } @article{13138, abstract = {We consider the spin- 1 2 Heisenberg chain (XXX model) weakly perturbed away from integrability by an isotropic next-to-nearest neighbor exchange interaction. Recently, it was conjectured that this model possesses an infinite tower of quasiconserved integrals of motion (charges) [D. Kurlov et al., Phys. Rev. B 105, 104302 (2022)]. In this work we first test this conjecture by investigating how the norm of the adiabatic gauge potential (AGP) scales with the system size, which is known to be a remarkably accurate measure of chaos. We find that for the perturbed XXX chain the behavior of the AGP norm corresponds to neither an integrable nor a chaotic regime, which supports the conjectured quasi-integrability of the model. We then prove the conjecture and explicitly construct the infinite set of quasiconserved charges. Our proof relies on the fact that the XXX chain perturbed by next-to-nearest exchange interaction can be viewed as a truncation of an integrable long-range deformation of the Heisenberg spin chain.}, author = {Orlov, Pavel and Tiutiakina, Anastasiia and Sharipov, Rustem and Petrova, Elena and Gritsev, Vladimir and Kurlov, Denis V.}, issn = {2469-9969}, journal = {Physical Review B}, number = {18}, publisher = {American Physical Society}, title = {{Adiabatic eigenstate deformations and weak integrability breaking of Heisenberg chain}}, doi = {10.1103/PhysRevB.107.184312}, volume = {107}, year = {2023}, } @article{13166, abstract = {Brachyury, a member of T-box gene family, is widely known for its major role in mesoderm specification in bilaterians. It is also present in non-bilaterian metazoans, such as cnidarians, where it acts as a component of an axial patterning system. In this study, we present a phylogenetic analysis of Brachyury genes within phylum Cnidaria, investigate differential expression and address a functional framework of Brachyury paralogs in hydrozoan Dynamena pumila. Our analysis indicates two duplication events of Brachyury within the cnidarian lineage. The first duplication likely appeared in the medusozoan ancestor, resulting in two copies in medusozoans, while the second duplication arose in the hydrozoan ancestor, resulting in three copies in hydrozoans. Brachyury1 and 2 display a conservative expression pattern marking the oral pole of the body axis in D. pumila. On the contrary, Brachyury3 expression was detected in scattered presumably nerve cells of the D. pumila larva. Pharmacological modulations indicated that Brachyury3 is not under regulation of cWnt signaling in contrast to the other two Brachyury genes. Divergence in expression patterns and regulation suggest neofunctionalization of Brachyury3 in hydrozoans.}, author = {Vetrova, Alexandra A. and Kupaeva, Daria M. and Kizenko, Alena and Lebedeva, Tatiana S. and Walentek, Peter and Tsikolia, Nikoloz and Kremnyov, Stanislav V.}, issn = {2045-2322}, journal = {Scientific Reports}, publisher = {Springer Nature}, title = {{The evolutionary history of Brachyury genes in Hydrozoa involves duplications, divergence, and neofunctionalization}}, doi = {10.1038/s41598-023-35979-8}, volume = {13}, year = {2023}, } @phdthesis{13175, abstract = {About a 100 years ago, we discovered that our universe is inherently noisy, that is, measuring any physical quantity with a precision beyond a certain point is not possible because of an omnipresent inherent noise. We call this - the quantum noise. Certain physical processes allow this quantum noise to get correlated in conjugate physical variables. These quantum correlations can be used to go beyond the potential of our inherently noisy universe and obtain a quantum advantage over the classical applications. Quantum noise being inherent also means that, at the fundamental level, the physical quantities are not well defined and therefore, objects can stay in multiple states at the same time. For example, the position of a particle not being well defined means that the particle is in multiple positions at the same time. About 4 decades ago, we started exploring the possibility of using objects which can be in multiple states at the same time to increase the dimensionality in computation. Thus, the field of quantum computing was born. We discovered that using quantum entanglement, a property closely related to quantum correlations, can be used to speed up computation of certain problems, such as factorisation of large numbers, faster than any known classical algorithm. Thus began the pursuit to make quantum computers a reality. Till date, we have explored quantum control over many physical systems including photons, spins, atoms, ions and even simple circuits made up of superconducting material. However, there persists one ubiquitous theme. The more readily a system interacts with an external field or matter, the more easily we can control it. But this also means that such a system can easily interact with a noisy environment and quickly lose its coherence. Consequently, such systems like electron spins need to be protected from the environment to ensure the longevity of their coherence. Other systems like nuclear spins are naturally protected as they do not interact easily with the environment. But, due to the same reason, it is harder to interact with such systems. After decades of experimentation with various systems, we are convinced that no one type of quantum system would be the best for all the quantum applications. We would need hybrid systems which are all interconnected - much like the current internet where all sorts of devices can all talk to each other - but now for quantum devices. A quantum internet. Optical photons are the best contenders to carry information for the quantum internet. They can carry quantum information cheaply and without much loss - the same reasons which has made them the backbone of our current internet. Following this direction, many systems, like trapped ions, have already demonstrated successful quantum links over a large distances using optical photons. However, some of the most promising contenders for quantum computing which are based on microwave frequencies have been left behind. This is because high energy optical photons can adversely affect fragile low-energy microwave systems. In this thesis, we present substantial progress on this missing quantum link between microwave and optics using electrooptical nonlinearities in lithium niobate. The nonlinearities are enhanced by using resonant cavities for all the involved modes leading to observation of strong direct coupling between optical and microwave frequencies. With this strong coupling we are not only able to achieve almost 100\% internal conversion efficiency with low added noise, thus presenting a quantum-enabled transducer, but also we are able to observe novel effects such as cooling of a microwave mode using optics. The strong coupling regime also leads to direct observation of dynamical backaction effect between microwave and optical frequencies which are studied in detail here. Finally, we also report first observation of microwave-optics entanglement in form of two-mode squeezed vacuum squeezed 0.7dB below vacuum level. With this new bridge between microwave and optics, the microwave-based quantum technologies can finally be a part of a quantum network which is based on optical photons - putting us one step closer to a future with quantum internet. }, author = {Sahu, Rishabh}, isbn = {978-3-99078-030-5}, issn = {2663 - 337X}, keywords = {quantum optics, electrooptics, quantum networks, quantum communication, transduction}, pages = {202}, publisher = {Institute of Science and Technology Austria}, title = {{Cavity quantum electrooptics}}, doi = {10.15479/at:ista:13175}, year = {2023}, } @article{13207, abstract = {We consider the linear BCS equation, determining the BCS critical temperature, in the presence of a boundary, where Dirichlet boundary conditions are imposed. In the one-dimensional case with point interactions, we prove that the critical temperature is strictly larger than the bulk value, at least at weak coupling. In particular, the Cooper-pair wave function localizes near the boundary, an effect that cannot be modeled by effective Neumann boundary conditions on the order parameter as often imposed in Ginzburg–Landau theory. We also show that the relative shift in critical temperature vanishes if the coupling constant either goes to zero or to infinity.}, author = {Hainzl, Christian and Roos, Barbara and Seiringer, Robert}, issn = {1664-0403}, journal = {Journal of Spectral Theory}, number = {4}, pages = {1507–1540}, publisher = {EMS Press}, title = {{Boundary superconductivity in the BCS model}}, doi = {10.4171/JST/439}, volume = {12}, year = {2023}, } @inproceedings{13221, abstract = {The safety-liveness dichotomy is a fundamental concept in formal languages which plays a key role in verification. Recently, this dichotomy has been lifted to quantitative properties, which are arbitrary functions from infinite words to partially-ordered domains. We look into harnessing the dichotomy for the specific classes of quantitative properties expressed by quantitative automata. These automata contain finitely many states and rational-valued transition weights, and their common value functions Inf, Sup, LimInf, LimSup, LimInfAvg, LimSupAvg, and DSum map infinite words into the totallyordered domain of real numbers. In this automata-theoretic setting, we establish a connection between quantitative safety and topological continuity and provide an alternative characterization of quantitative safety and liveness in terms of their boolean counterparts. For all common value functions, we show how the safety closure of a quantitative automaton can be constructed in PTime, and we provide PSpace-complete checks of whether a given quantitative automaton is safe or live, with the exception of LimInfAvg and LimSupAvg automata, for which the safety check is in ExpSpace. Moreover, for deterministic Sup, LimInf, and LimSup automata, we give PTime decompositions into safe and live automata. These decompositions enable the separation of techniques for safety and liveness verification for quantitative specifications.}, author = {Boker, Udi and Henzinger, Thomas A and Mazzocchi, Nicolas Adrien and Sarac, Naci E}, booktitle = {34th International Conference on Concurrency Theory}, isbn = {9783959772990}, issn = {1868-8969}, location = {Antwerp, Belgium}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Safety and liveness of quantitative automata}}, doi = {10.4230/LIPIcs.CONCUR.2023.17}, volume = {279}, year = {2023}, } @inproceedings{13262, abstract = {Determining the degree of inherent parallelism in classical sequential algorithms and leveraging it for fast parallel execution is a key topic in parallel computing, and detailed analyses are known for a wide range of classical algorithms. In this paper, we perform the first such analysis for the fundamental Union-Find problem, in which we are given a graph as a sequence of edges, and must maintain its connectivity structure under edge additions. We prove that classic sequential algorithms for this problem are well-parallelizable under reasonable assumptions, addressing a conjecture by [Blelloch, 2017]. More precisely, we show via a new potential argument that, under uniform random edge ordering, parallel union-find operations are unlikely to interfere: T concurrent threads processing the graph in parallel will encounter memory contention O(T2 · log |V| · log |E|) times in expectation, where |E| and |V| are the number of edges and nodes in the graph, respectively. We leverage this result to design a new parallel Union-Find algorithm that is both internally deterministic, i.e., its results are guaranteed to match those of a sequential execution, but also work-efficient and scalable, as long as the number of threads T is O(|E|1 over 3 - ε), for an arbitrarily small constant ε > 0, which holds for most large real-world graphs. We present lower bounds which show that our analysis is close to optimal, and experimental results suggesting that the performance cost of internal determinism is limited.}, author = {Fedorov, Alexander and Hashemi, Diba and Nadiradze, Giorgi and Alistarh, Dan-Adrian}, booktitle = {Proceedings of the 35th ACM Symposium on Parallelism in Algorithms and Architectures}, isbn = {9781450395458}, location = {Orlando, FL, United States}, pages = {261--271}, publisher = {Association for Computing Machinery}, title = {{Provably-efficient and internally-deterministic parallel Union-Find}}, doi = {10.1145/3558481.3591082}, year = {2023}, } @article{13274, abstract = {Viscous flows through pipes and channels are steady and ordered until, with increasing velocity, the laminar motion catastrophically breaks down and gives way to turbulence. How this apparently discontinuous change from low- to high-dimensional motion can be rationalized within the framework of the Navier-Stokes equations is not well understood. Exploiting geometrical properties of transitional channel flow we trace turbulence to far lower Reynolds numbers (Re) than previously possible and identify the complete path that reversibly links fully turbulent motion to an invariant solution. This precursor of turbulence destabilizes rapidly with Re, and the accompanying explosive increase in attractor dimension effectively marks the transition between deterministic and de facto stochastic dynamics.}, author = {Paranjape, Chaitanya S and Yalniz, Gökhan and Duguet, Yohann and Budanur, Nazmi B and Hof, Björn}, issn = {1079-7114}, journal = {Physical Review Letters}, keywords = {General Physics and Astronomy}, number = {3}, publisher = {American Physical Society}, title = {{Direct path from turbulence to time-periodic solutions}}, doi = {10.1103/physrevlett.131.034002}, volume = {131}, year = {2023}, } @phdthesis{13286, abstract = {Semiconductor-superconductor hybrid systems are the harbour of many intriguing mesoscopic phenomena. This material combination leads to spatial variations of the superconducting properties, which gives rise to Andreev bound states (ABSs). Some of these states might exhibit remarkable properties that render them highly desirable for topological quantum computing. The most prominent and hunted of such states are Majorana zero modes (MZMs), quasiparticles equals to their own quasiparticles that they follow non-abelian statistics. In this thesis, we first introduce the general framework of such hybrid systems and, then, we unveil a series of mesoscopic phenomena that we discovered. Firstly, we show tunneling spectroscopy experiments on full-shell nanowires (NWs) showing that unwanted quantum-dot states coupled to superconductors (Yu-Shiba-Rusinov states) can mimic MZMs signatures. Then, we introduce a novel protocol which allowed the integration of tunneling spectroscopy with Coulomb spectroscopy within the same device. Employing this approach on both full-shell NWs and partial-shell NWs, we demonstrated that longitudinally confined states reveal charge transport phenomenology similar to the one expected for MZMs. These findings shed light on the intricate interplay between superconductivity and quantum confinement, which brought us to explore another material platform, i.e. a two-dimensional Germanium hole gas. After developing a robust way to induce superconductivity in such system, we showed how to engineer the proximity effect and we revealed a superconducting hard gap. Finally, we created a superconducting radio frequency driven ideal diode and a generator of non-sinusoidal current-phase relations. Our results open the path for the exploration of protected superconducting qubits and more complex hybrid devices in planar Germanium, like Kitaev chains and hybrid qubit devices.}, author = {Valentini, Marco}, issn = {2663 - 337X}, pages = {184}, publisher = {Institute of Science and Technology Austria}, title = {{Mesoscopic phenomena in hybrid semiconductor-superconductor nanodevices : From full-shell nanowires to two-dimensional hole gas in germanium}}, doi = {10.15479/at:ista:13286}, year = {2023}, } @inproceedings{13292, abstract = {The operator precedence languages (OPLs) represent the largest known subclass of the context-free languages which enjoys all desirable closure and decidability properties. This includes the decidability of language inclusion, which is the ultimate verification problem. Operator precedence grammars, automata, and logics have been investigated and used, for example, to verify programs with arithmetic expressions and exceptions (both of which are deterministic pushdown but lie outside the scope of the visibly pushdown languages). In this paper, we complete the picture and give, for the first time, an algebraic characterization of the class of OPLs in the form of a syntactic congruence that has finitely many equivalence classes exactly for the operator precedence languages. This is a generalization of the celebrated Myhill-Nerode theorem for the regular languages to OPLs. As one of the consequences, we show that universality and language inclusion for nondeterministic operator precedence automata can be solved by an antichain algorithm. Antichain algorithms avoid determinization and complementation through an explicit subset construction, by leveraging a quasi-order on words, which allows the pruning of the search space for counterexample words without sacrificing completeness. Antichain algorithms can be implemented symbolically, and these implementations are today the best-performing algorithms in practice for the inclusion of finite automata. We give a generic construction of the quasi-order needed for antichain algorithms from a finite syntactic congruence. This yields the first antichain algorithm for OPLs, an algorithm that solves the ExpTime-hard language inclusion problem for OPLs in exponential time.}, author = {Henzinger, Thomas A and Kebis, Pavol and Mazzocchi, Nicolas Adrien and Sarac, Naci E}, booktitle = {50th International Colloquium on Automata, Languages, and Programming}, isbn = {9783959772785}, issn = {1868-8969}, location = {Paderborn, Germany}, pages = {129:1----129:20}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Regular methods for operator precedence languages}}, doi = {10.4230/LIPIcs.ICALP.2023.129}, volume = {261}, year = {2023}, } @inproceedings{13310, abstract = {Machine-learned systems are in widespread use for making decisions about humans, and it is important that they are fair, i.e., not biased against individuals based on sensitive attributes. We present runtime verification of algorithmic fairness for systems whose models are unknown, but are assumed to have a Markov chain structure. We introduce a specification language that can model many common algorithmic fairness properties, such as demographic parity, equal opportunity, and social burden. We build monitors that observe a long sequence of events as generated by a given system, and output, after each observation, a quantitative estimate of how fair or biased the system was on that run until that point in time. The estimate is proven to be correct modulo a variable error bound and a given confidence level, where the error bound gets tighter as the observed sequence gets longer. Our monitors are of two types, and use, respectively, frequentist and Bayesian statistical inference techniques. While the frequentist monitors compute estimates that are objectively correct with respect to the ground truth, the Bayesian monitors compute estimates that are correct subject to a given prior belief about the system’s model. Using a prototype implementation, we show how we can monitor if a bank is fair in giving loans to applicants from different social backgrounds, and if a college is fair in admitting students while maintaining a reasonable financial burden on the society. Although they exhibit different theoretical complexities in certain cases, in our experiments, both frequentist and Bayesian monitors took less than a millisecond to update their verdicts after each observation.}, author = {Henzinger, Thomas A and Karimi, Mahyar and Kueffner, Konstantin and Mallik, Kaushik}, booktitle = {Computer Aided Verification}, isbn = {9783031377020}, issn = {1611-3349}, location = {Paris, France}, pages = {358–382}, publisher = {Springer Nature}, title = {{Monitoring algorithmic fairness}}, doi = {10.1007/978-3-031-37703-7_17}, volume = {13965}, year = {2023}, } @article{13314, abstract = {The emergence of large-scale order in self-organized systems relies on local interactions between individual components. During bacterial cell division, FtsZ—a prokaryotic homologue of the eukaryotic protein tubulin—polymerizes into treadmilling filaments that further organize into a cytoskeletal ring. In vitro, FtsZ filaments can form dynamic chiral assemblies. However, how the active and passive properties of individual filaments relate to these large-scale self-organized structures remains poorly understood. Here we connect single-filament properties with the mesoscopic scale by combining minimal active matter simulations and biochemical reconstitution experiments. We show that the density and flexibility of active chiral filaments define their global order. At intermediate densities, curved, flexible filaments organize into chiral rings and polar bands. An effectively nematic organization dominates for high densities and for straight, mutant filaments with increased rigidity. Our predicted phase diagram quantitatively captures these features, demonstrating how the flexibility, density and chirality of the active filaments affect their collective behaviour. Our findings shed light on the fundamental properties of active chiral matter and explain how treadmilling FtsZ filaments organize during bacterial cell division.}, author = {Dunajova, Zuzana and Prats Mateu, Batirtze and Radler, Philipp and Lim, Keesiang and Brandis, Dörte and Velicky, Philipp and Danzl, Johann G and Wong, Richard W. and Elgeti, Jens and Hannezo, Edouard B and Loose, Martin}, issn = {1745-2481}, journal = {Nature Physics}, pages = {1916--1926}, publisher = {Springer Nature}, title = {{Chiral and nematic phases of flexible active filaments}}, doi = {10.1038/s41567-023-02218-w}, volume = {19}, year = {2023}, } @phdthesis{13331, abstract = {The extension of extremal combinatorics to the setting of exterior algebra is a work in progress that gained attention recently. In this thesis, we study the combinatorial structure of exterior algebra by introducing a dictionary that translates the notions from the set systems into the framework of exterior algebra. We show both generalizations of celebrated Erdös--Ko--Rado theorem and Hilton--Milner theorem to the setting of exterior algebra in the simplest non-trivial case of two-forms. }, author = {Köse, Seyda}, issn = {2791-4585}, pages = {26}, publisher = {Institute of Science and Technology Austria}, title = {{Exterior algebra and combinatorics}}, doi = {10.15479/at:ista:13331}, year = {2023}, } @phdthesis{13984, abstract = {Social insects fight disease using their individual immune systems and the cooperative sanitary behaviors of colony members. These social defenses are well explored against externally-infecting pathogens, but little is known about defense strategies against internally-infecting pathogens, such as viruses. Viruses are ubiquitous and in the last decades it has become evident that also many ant species harbor viruses. We present one of the first studies addressing transmission dynamics and collective disease defenses against viruses in ants on a mechanistic level. I successfully established an experimental ant host – viral pathogen system as a model for the defense strategies used by social insects against internal pathogen infections, as outlined in the third chapter. In particular, we studied how garden ants (Lasius neglectus) defend themselves and their colonies against the generalist insect virus CrPV (cricket paralysis virus). We chose microinjections of virus directly into the ants’ hemolymph because it allowed us to use a defined exposure dose. Here we show that this is a good model system, as the virus is replicating and thus infecting the host. The ants mount a clear individual immune response against the viral infection, which is characterized by a specific siRNA pattern, namely siRNAs mapping against the viral genome with a peak of 21 and 22 bp long fragments. The onset of this immune response is consistent with the timeline of viral replication that starts already within two days post injection. The disease manifests in decreased survival over a course of two to three weeks. Regarding group living, we find that infected ants show a strong individual immune response, but that their course of disease is little affected by nestmate presence, as described in chapter four. Hence, we do not find social immunity in the context of viral infections in ants. Nestmates, however, can contract the virus. Using Drosophila S2R+ cells in culture, we showed that 94 % of the nestmates contract active virus within four days of social contact to an infected individual. Virus is transmitted in low doses, thus not causing disease transmission within the colony. While virus can be transmitted during short direct contacts, we also assume transmission from deceased ants and show that the nestmates’ immune system gets activated after contracting a low viral dose. We find considerable potential for indirect transmission via the nest space. Virus is shed to the nest, where it stays viable for one week and is also picked up by other ants. Apart from that, we want to underline the potential of ant poison as antiviral agent. We determined that ant poison successfully inactivates CrPV in vitro. However, we found no evidence for effective poison use to sanitize the nest space. On the other hand, local application of ant poison by oral poison uptake, which is part of the ants prophylactic behavioral repertoire, probably contributes to keeping the gut of each individual sanitized. We hypothesize that oral poison uptake might be the reason why we did not find viable virus in the trophallactic fluid. The fifth chapter encompasses preliminary data on potential social immunization. However, our experiments do not confirm an actual survival benefit for the nestmates upon pathogen challenge under the given experimental settings. Nevertheless, we do not want to rule out the possibility for nestmate immunization, but rather emphasize that considering different experimental timelines and viral doses would provide a multitude of options for follow-up experiments. In conclusion, we find that prophylactic individual behaviors, such as oral poison uptake, might play a role in preventing viral disease transmission. Compared to colony defense against external pathogens, internal pathogen infections require a stronger component of individual physiological immunity than behavioral social immunity, yet could still lead to collective protection.}, author = {Franschitz, Anna}, isbn = {978-3-99078-034-3}, issn = {2663 - 337X}, pages = {89}, publisher = {Institute of Science and Technology Austria}, title = {{Individual and social immunity against viral infections in ants}}, doi = {10.15479/at:ista:13984}, year = {2023}, }