TY - JOUR
AB - We investigate the quantum interference shifts between energetically close states, where the state structure is observed by laser spectroscopy. We report a compact and analytical expression that models the quantum interference induced shift for any admixture of circular polarization of the incident laser and angle of observation. An experimental scenario free of quantum interference can thus be predicted with this formula. Although this study is exemplified here for muonic deuterium, it can be applied to any other laser spectroscopy measurement of ns-n′p frequencies of a nonrelativistic atomic system, via an ns→n′p→n′′s scheme.
AU - Amaro, Pedro
AU - Fratini, Filippo
AU - Safari, Laleh
AU - Antognini, Aldo
AU - Indelicato, Paul
AU - Pohl, Randolf
AU - Santos, José
ID - 1587
IS - 6
JF - Physical Review A - Atomic, Molecular, and Optical Physics
TI - Quantum interference shifts in laser spectroscopy with elliptical polarization
VL - 92
ER -
TY - JOUR
AB - We investigate the Taylor-Couette system where the radius ratio is close to unity. Systematically increasing the Reynolds number, we observe a number of previously known transitions, such as one from the classical Taylor vortex flow (TVF) to wavy vortex flow (WVF) and the transition to fully developed turbulence. Prior to the onset of turbulence, we observe intermittent bursting patterns of localized turbulent patches, confirming the experimentally observed pattern of very short wavelength bursts (VSWBs). A striking finding is that, for a Reynolds number larger than that for the onset of VSWBs, a new type of intermittently bursting behavior emerges: patterns of azimuthally closed rings of various orders. We call them ring-bursting patterns, which surround the cylinder completely but remain localized and separated in the axial direction through nonturbulent wavy structures. We employ a number of quantitative measures including the cross-flow energy to characterize the ring-bursting patterns and to distinguish them from the background flow. These patterns are interesting because they do not occur in the wide-gap Taylor-Couette flow systems. The narrow-gap regime is less studied but certainly deserves further attention to gain deeper insights into complex flow dynamics in fluids.
AU - Altmeyer, Sebastian
AU - Do, Younghae
AU - Lai, Ying
ID - 1588
IS - 5
JF - Physical Review E
TI - Ring-bursting behavior en route to turbulence in narrow-gap Taylor-Couette flows
VL - 92
ER -
TY - JOUR
AB - We investigate the dynamics of ferrofluidic wavy vortex flows in the counter-rotating Taylor-Couette system, with a focus on wavy flows with a mixture of the dominant azimuthal modes. Without external magnetic field flows are stable and pro-grade with respect to the rotation of the inner cylinder. More complex behaviors can arise when an axial or a transverse magnetic field is applied. Depending on the direction and strength of the field, multi-stable wavy states and bifurcations can occur. We uncover the phenomenon of flow pattern reversal as the strength of the magnetic field is increased through a critical value. In between the regimes of pro-grade and retrograde flow rotations, standing waves with zero angular velocities can emerge. A striking finding is that, under a transverse magnetic field, a second reversal in the flow pattern direction can occur, where the flow pattern evolves into pro-grade rotation again from a retrograde state. Flow reversal is relevant to intriguing phenomena in nature such as geomagnetic reversal. Our results suggest that, in ferrofluids, flow pattern reversal can be induced by varying a magnetic field in a controlled manner, which can be realized in laboratory experiments with potential applications in the development of modern fluid devices.
AU - Altmeyer, Sebastian
AU - Do, Younghae
AU - Lai, Ying
ID - 1589
JF - Scientific Reports
TI - Magnetic field induced flow pattern reversal in a ferrofluidic Taylor-Couette system
VL - 5
ER -
TY - CHAP
AB - The straight skeleton of a polygon is the geometric graph obtained by tracing the vertices during a mitered offsetting process. It is known that the straight skeleton of a simple polygon is a tree, and one can naturally derive directions on the edges of the tree from the propagation of the shrinking process. In this paper, we ask the reverse question: Given a tree with directed edges, can it be the straight skeleton of a polygon? And if so, can we find a suitable simple polygon? We answer these questions for all directed trees where the order of edges around each node is fixed.
AU - Aichholzer, Oswin
AU - Biedl, Therese
AU - Hackl, Thomas
AU - Held, Martin
AU - Huber, Stefan
AU - Palfrader, Peter
AU - Vogtenhuber, Birgit
ID - 1590
T2 - Graph Drawing and Network Visualization
TI - Representing directed trees as straight skeletons
VL - 9411
ER -
TY - JOUR
AB - Auxin participates in a multitude of developmental processes, as well as responses to environmental cues. Compared with other plant hormones, auxin exhibits a unique property, as it undergoes directional, cell-to-cell transport facilitated by plasma membrane-localized transport proteins. Among them, a prominent role has been ascribed to the PIN family of auxin efflux facilitators. PIN proteins direct polar auxin transport on account of their asymmetric subcellular localizations. In this review, we provide an overview of the multiple developmental roles of PIN proteins, including the atypical endoplasmic reticulum-localized members of the family, and look at the family from an evolutionary perspective. Next, we cover the cell biological and molecular aspects of PIN function, in particular the establishment of their polar subcellular localization. Hormonal and environmental inputs into the regulation of PIN action are summarized as well.
AU - Adamowski, Maciek
AU - Friml, Jirí
ID - 1591
IS - 1
JF - Plant Cell
TI - PIN-dependent auxin transport: Action, regulation, and evolution
VL - 27
ER -
TY - JOUR
AB - Plants are sessile organisms that are permanently restricted to their site of germination. To compensate for their lack of mobility, plants evolved unique mechanisms enabling them to rapidly react to ever changing environmental conditions and flexibly adapt their postembryonic developmental program. A prominent demonstration of this developmental plasticity is their ability to bend organs in order to reach the position most optimal for growth and utilization of light, nutrients, and other resources. Shortly after germination, dicotyledonous seedlings form a bended structure, the so-called apical hook, to protect the delicate shoot meristem and cotyledons from damage when penetrating through the soil. Upon perception of a light stimulus, the apical hook rapidly opens and the photomorphogenic developmental program is activated. After germination, plant organs are able to align their growth with the light source and adopt the most favorable orientation through bending, in a process named phototropism. On the other hand, when roots and shoots are diverted from their upright orientation, they immediately detect a change in the gravity vector and bend to maintain a vertical growth direction. Noteworthy, despite the diversity of external stimuli perceived by different plant organs, all plant tropic movements share a common mechanistic basis: differential cell growth. In our review, we will discuss the molecular principles underlying various tropic responses with the focus on mechanisms mediating the perception of external signals, transduction cascades and downstream responses that regulate differential cell growth and consequently, organ bending. In particular, we highlight common and specific features of regulatory pathways in control of the bending of organs and a role for the plant hormone auxin as a key regulatory component.
AU - Žádníková, Petra
AU - Smet, Dajo
AU - Zhu, Qiang
AU - Van Der Straeten, Dominique
AU - Benková, Eva
ID - 1593
IS - 4
JF - Frontiers in Plant Science
TI - Strategies of seedlings to overcome their sessile nature: Auxin in mobility control
VL - 6
ER -
TY - CONF
AB - Quantitative extensions of temporal logics have recently attracted significant attention. In this work, we study frequency LTL (fLTL), an extension of LTL which allows to speak about frequencies of events along an execution. Such an extension is particularly useful for probabilistic systems that often cannot fulfil strict qualitative guarantees on the behaviour. It has been recently shown that controller synthesis for Markov decision processes and fLTL is decidable when all the bounds on frequencies are 1. As a step towards a complete quantitative solution, we show that the problem is decidable for the fragment fLTL\GU, where U does not occur in the scope of G (but still F can). Our solution is based on a novel translation of such quantitative formulae into equivalent deterministic automata.
AU - Forejt, Vojtěch
AU - Krčál, Jan
AU - Kretinsky, Jan
ID - 1594
TI - Controller synthesis for MDPs and frequency LTL\GU
VL - 9450
ER -
TY - CONF
AB - A drawing of a graph G is radial if the vertices of G are placed on concentric circles C1, . . . , Ck with common center c, and edges are drawn radially: every edge intersects every circle centered at c at most once. G is radial planar if it has a radial embedding, that is, a crossing- free radial drawing. If the vertices of G are ordered or partitioned into ordered levels (as they are for leveled graphs), we require that the assignment of vertices to circles corresponds to the given ordering or leveling. We show that a graph G is radial planar if G has a radial drawing in which every two edges cross an even number of times; the radial embedding has the same leveling as the radial drawing. In other words, we establish the weak variant of the Hanani-Tutte theorem for radial planarity. This generalizes a result by Pach and Tóth.
AU - Fulek, Radoslav
AU - Pelsmajer, Michael
AU - Schaefer, Marcus
ID - 1595
TI - Hanani-Tutte for radial planarity
VL - 9411
ER -
TY - CONF
AB - Let C={C1,...,Cn} denote a collection of translates of a regular convex k-gon in the plane with the stacking order. The collection C forms a visibility clique if for everyi < j the intersection Ci and (Ci ∩ Cj)\⋃i<l<jCl =∅.elements that are stacked between them, i.e., We show that if C forms a visibility clique its size is bounded from above by O(k4) thereby improving the upper bound of 22k from the aforementioned paper. We also obtain an upper bound of 22(k/2)+2 on the size of a visibility clique for homothetes of a convex (not necessarily regular) k-gon.
AU - Fulek, Radoslav
AU - Radoičić, Radoš
ID - 1596
TI - Vertical visibility among parallel polygons in three dimensions
VL - 9411
ER -
TY - JOUR
AB - We consider Markov decision processes (MDPs) with specifications given as Büchi (liveness) objectives, and examine the problem of computing the set of almost-sure winning vertices such that the objective can be ensured with probability 1 from these vertices. We study for the first time the average-case complexity of the classical algorithm for computing the set of almost-sure winning vertices for MDPs with Büchi objectives. Our contributions are as follows: First, we show that for MDPs with constant out-degree the expected number of iterations is at most logarithmic and the average-case running time is linear (as compared to the worst-case linear number of iterations and quadratic time complexity). Second, for the average-case analysis over all MDPs we show that the expected number of iterations is constant and the average-case running time is linear (again as compared to the worst-case linear number of iterations and quadratic time complexity). Finally we also show that when all MDPs are equally likely, the probability that the classical algorithm requires more than a constant number of iterations is exponentially small.
AU - Chatterjee, Krishnendu
AU - Joglekar, Manas
AU - Shah, Nisarg
ID - 1598
IS - 3
JF - Theoretical Computer Science
TI - Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives
VL - 573
ER -
TY - CONF
AB - We propose a flexible exchange format for ω-automata, as typically used in formal verification, and implement support for it in a range of established tools. Our aim is to simplify the interaction of tools, helping the research community to build upon other people’s work. A key feature of the format is the use of very generic acceptance conditions, specified by Boolean combinations of acceptance primitives, rather than being limited to common cases such as Büchi, Streett, or Rabin. Such flexibility in the choice of acceptance conditions can be exploited in applications, for example in probabilistic model checking, and furthermore encourages the development of acceptance-agnostic tools for automata manipulations. The format allows acceptance conditions that are either state-based or transition-based, and also supports alternating automata.
AU - Babiak, Tomáš
AU - Blahoudek, František
AU - Duret Lutz, Alexandre
AU - Klein, Joachim
AU - Kretinsky, Jan
AU - Mueller, Daniel
AU - Parker, David
AU - Strejček, Jan
ID - 1601
TI - The Hanoi omega-automata format
VL - 9206
ER -
TY - JOUR
AB - Interprocedural analysis is at the heart of numerous applications in programming languages, such as alias analysis, constant propagation, etc. Recursive state machines (RSMs) are standard models for interprocedural analysis. We consider a general framework with RSMs where the transitions are labeled from a semiring, and path properties are algebraic with semiring operations. RSMs with algebraic path properties can model interprocedural dataflow analysis problems, the shortest path problem, the most probable path problem, etc. The traditional algorithms for interprocedural analysis focus on path properties where the starting point is fixed as the entry point of a specific method. In this work, we consider possible multiple queries as required in many applications such as in alias analysis. The study of multiple queries allows us to bring in a very important algorithmic distinction between the resource usage of the one-time preprocessing vs for each individual query. The second aspect that we consider is that the control flow graphs for most programs have constant treewidth. Our main contributions are simple and implementable algorithms that supportmultiple queries for algebraic path properties for RSMs that have constant treewidth. Our theoretical results show that our algorithms have small additional one-time preprocessing, but can answer subsequent queries significantly faster as compared to the current best-known solutions for several important problems, such as interprocedural reachability and shortest path. We provide a prototype implementation for interprocedural reachability and intraprocedural shortest path that gives a significant speed-up on several benchmarks.
AU - Chatterjee, Krishnendu
AU - Ibsen-Jensen, Rasmus
AU - Pavlogiannis, Andreas
AU - Goyal, Prateesh
ID - 1602
IS - 1
JF - ACM SIGPLAN Notices
TI - Faster algorithms for algebraic path properties in recursive state machines with constant treewidth
VL - 50
ER -
TY - CONF
AB - For deterministic systems, a counterexample to a property can simply be an error trace, whereas counterexamples in probabilistic systems are necessarily more complex. For instance, a set of erroneous traces with a sufficient cumulative probability mass can be used. Since these are too large objects to understand and manipulate, compact representations such as subchains have been considered. In the case of probabilistic systems with non-determinism, the situation is even more complex. While a subchain for a given strategy (or scheduler, resolving non-determinism) is a straightforward choice, we take a different approach. Instead, we focus on the strategy itself, and extract the most important decisions it makes, and present its succinct representation.
The key tools we employ to achieve this are (1) introducing a concept of importance of a state w.r.t. the strategy, and (2) learning using decision trees. There are three main consequent advantages of our approach. Firstly, it exploits the quantitative information on states, stressing the more important decisions. Secondly, it leads to a greater variability and degree of freedom in representing the strategies. Thirdly, the representation uses a self-explanatory data structure. In summary, our approach produces more succinct and more explainable strategies, as opposed to e.g. binary decision diagrams. Finally, our experimental results show that we can extract several rules describing the strategy even for very large systems that do not fit in memory, and based on the rules explain the erroneous behaviour.
AU - Brázdil, Tomáš
AU - Chatterjee, Krishnendu
AU - Chmelik, Martin
AU - Fellner, Andreas
AU - Kretinsky, Jan
ID - 1603
TI - Counterexample explanation by learning small strategies in Markov decision processes
VL - 9206
ER -
TY - JOUR
AB - We consider the quantitative analysis problem for interprocedural control-flow graphs (ICFGs). The input consists of an ICFG, a positive weight function that assigns every transition a positive integer-valued number, and a labelling of the transitions (events) as good, bad, and neutral events. The weight function assigns to each transition a numerical value that represents ameasure of how good or bad an event is. The quantitative analysis problem asks whether there is a run of the ICFG where the ratio of the sum of the numerical weights of good events versus the sum of weights of bad events in the long-run is at least a given threshold (or equivalently, to compute the maximal ratio among all valid paths in the ICFG). The quantitative analysis problem for ICFGs can be solved in polynomial time, and we present an efficient and practical algorithm for the problem. We show that several problems relevant for static program analysis, such as estimating the worst-case execution time of a program or the average energy consumption of a mobile application, can be modeled in our framework. We have implemented our algorithm as a tool in the Java Soot framework. We demonstrate the effectiveness of our approach with two case studies. First, we show that our framework provides a sound approach (no false positives) for the analysis of inefficiently-used containers. Second, we show that our approach can also be used for static profiling of programs which reasons about methods that are frequently invoked. Our experimental results show that our tool scales to relatively large benchmarks, and discovers relevant and useful information that can be used to optimize performance of the programs.
AU - Chatterjee, Krishnendu
AU - Pavlogiannis, Andreas
AU - Velner, Yaron
ID - 1604
IS - 1
JF - Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT
SN - 978-1-4503-3300-9
TI - Quantitative interprocedural analysis
VL - 50
ER -
TY - CONF
AB - Multiaffine hybrid automata (MHA) represent a powerful formalism to model complex dynamical systems. This formalism is particularly suited for the representation of biological systems which often exhibit highly non-linear behavior. In this paper, we consider the problem of parameter identification for MHA. We present an abstraction of MHA based on linear hybrid automata, which can be analyzed by the SpaceEx model checker. This abstraction enables a precise handling of time-dependent properties. We demonstrate the potential of our approach on a model of a genetic regulatory network and a myocyte model.
AU - Bogomolov, Sergiy
AU - Schilling, Christian
AU - Bartocci, Ezio
AU - Batt, Grégory
AU - Kong, Hui
AU - Grosu, Radu
ID - 1605
TI - Abstraction-based parameter synthesis for multiaffine systems
VL - 9434
ER -
TY - CONF
AB - In this paper, we present the first steps toward a runtime verification framework for monitoring hybrid and cyber-physical systems (CPS) development tools based on randomized differential testing. The development tools include hybrid systems reachability analysis tools, model-based development environments like Simulink/Stateflow (SLSF), etc. First, hybrid automaton models are randomly generated. Next, these hybrid automaton models are translated to a number of different tools (currently, SpaceEx, dReach, Flow*, HyCreate, and the MathWorks’ Simulink/Stateflow) using the HyST source transformation and translation tool. Then, the hybrid automaton models are executed in the different tools and their outputs are parsed. The final step is the differential comparison: the outputs of the different tools are compared. If the results do not agree (in the sense that an analysis or verification result from one tool does not match that of another tool, ignoring timeouts, etc.), a candidate bug is flagged and the model is saved for future analysis by the user. The process then repeats and the monitoring continues until the user terminates the process. We present preliminary results that have been useful in identifying a few bugs in the analysis methods of different development tools, and in an earlier version of HyST.
AU - Nguyen, Luan
AU - Schilling, Christian
AU - Bogomolov, Sergiy
AU - Johnson, Taylor
ID - 1606
TI - Runtime verification for hybrid analysis tools
VL - 9333
ER -
TY - CONF
AB - The synthesis problem asks for the automatic construction of a system from its specification. In the traditional setting, the system is “constructed from scratch” rather than composed from reusable components. However, this is rare in practice, and almost every non-trivial software system relies heavily on the use of libraries of reusable components. Recently, Lustig and Vardi introduced dataflow and controlflow synthesis from libraries of reusable components. They proved that dataflow synthesis is undecidable, while controlflow synthesis is decidable. The problem of controlflow synthesis from libraries of probabilistic components was considered by Nain, Lustig and Vardi, and was shown to be decidable for qualitative analysis (that asks that the specification be satisfied with probability 1). Our main contribution for controlflow synthesis from probabilistic components is to establish better complexity bounds for the qualitative analysis problem, and to show that the more general quantitative problem is undecidable. For the qualitative analysis, we show that the problem (i) is EXPTIME-complete when the specification is given as a deterministic parity word automaton, improving the previously known 2EXPTIME upper bound; and (ii) belongs to UP ∩ coUP and is parity-games hard, when the specification is given directly as a parity condition on the components, improving the previously known EXPTIME upper bound.
AU - Chatterjee, Krishnendu
AU - Doyen, Laurent
AU - Vardi, Moshe
ID - 1609
TI - The complexity of synthesis from probabilistic components
VL - 9135
ER -
TY - CONF
AB - The edit distance between two words w1, w2 is the minimal number of word operations (letter insertions, deletions, and substitutions) necessary to transform w1 to w2. The edit distance generalizes to languages L1,L2, where the edit distance is the minimal number k such that for every word from L1 there exists a word in L2 with edit distance at most k. We study the edit distance computation problem between pushdown automata and their subclasses. The problem of computing edit distance to pushdown automata is undecidable, and in practice, the interesting question is to compute the edit distance from a pushdown automaton (the implementation, a standard model for programs with recursion) to a regular language (the specification). In this work, we present a complete picture of decidability and complexity for deciding whether, for a given threshold k, the edit distance from a pushdown automaton to a finite automaton is at most k.
AU - Chatterjee, Krishnendu
AU - Henzinger, Thomas A
AU - Ibsen-Jensen, Rasmus
AU - Otop, Jan
ID - 1610
IS - Part II
TI - Edit distance for pushdown automata
VL - 9135
ER -
TY - JOUR
AB - Biosensors for signaling molecules allow the study of physiological processes by bringing together the fields of protein engineering, fluorescence imaging, and cell biology. Construction of genetically encoded biosensors generally relies on the availability of a binding "core" that is both specific and stable, which can then be combined with fluorescent molecules to create a sensor. However, binding proteins with the desired properties are often not available in nature and substantial improvement to sensors can be required, particularly with regard to their durability. Ancestral protein reconstruction is a powerful protein-engineering tool able to generate highly stable and functional proteins. In this work, we sought to establish the utility of ancestral protein reconstruction to biosensor development, beginning with the construction of an l-arginine biosensor. l-arginine, as the immediate precursor to nitric oxide, is an important molecule in many physiological contexts including brain function. Using a combination of ancestral reconstruction and circular permutation, we constructed a Förster resonance energy transfer (FRET) biosensor for l-arginine (cpFLIPR). cpFLIPR displays high sensitivity and specificity, with a Kd of ∼14 μM and a maximal dynamic range of 35%. Importantly, cpFLIPR was highly robust, enabling accurate l-arginine measurement at physiological temperatures. We established that cpFLIPR is compatible with two-photon excitation fluorescence microscopy and report l-arginine concentrations in brain tissue.
AU - Whitfield, Jason
AU - Zhang, William
AU - Herde, Michel
AU - Clifton, Ben
AU - Radziejewski, Johanna
AU - Janovjak, Harald L
AU - Henneberger, Christian
AU - Jackson, Colin
ID - 1611
IS - 9
JF - Protein Science
TI - Construction of a robust and sensitive arginine biosensor through ancestral protein reconstruction
VL - 24
ER -
TY - JOUR
AB - GABAergic perisoma-inhibiting fast-spiking interneurons (PIIs) effectively control the activity of large neuron populations by their wide axonal arborizations. It is generally assumed that the output of one PII to its target cells is strong and rapid. Here, we show that, unexpectedly, both strength and time course of PII-mediated perisomatic inhibition change with distance between synaptically connected partners in the rodent hippocampus. Synaptic signals become weaker due to lower contact numbers and decay more slowly with distance, very likely resulting from changes in GABAA receptor subunit composition. When distance-dependent synaptic inhibition is introduced to a rhythmically active neuronal network model, randomly driven principal cell assemblies are strongly synchronized by the PIIs, leading to higher precision in principal cell spike times than in a network with uniform synaptic inhibition.
AU - Strüber, Michael
AU - Jonas, Peter M
AU - Bartos, Marlene
ID - 1614
IS - 4
JF - PNAS
TI - Strength and duration of perisomatic GABAergic inhibition depend on distance between synaptically connected cells
VL - 112
ER -