@inproceedings{8623, abstract = {We introduce the monitoring of trace properties under assumptions. An assumption limits the space of possible traces that the monitor may encounter. An assumption may result from knowledge about the system that is being monitored, about the environment, or about another, connected monitor. We define monitorability under assumptions and study its theoretical properties. In particular, we show that for every assumption A, the boolean combinations of properties that are safe or co-safe relative to A are monitorable under A. We give several examples and constructions on how an assumption can make a non-monitorable property monitorable, and how an assumption can make a monitorable property monitorable with fewer resources, such as integer registers.}, author = {Henzinger, Thomas A and Sarac, Naci E}, booktitle = {Runtime Verification}, isbn = {9783030605070}, issn = {1611-3349}, location = {Los Angeles, CA, United States}, pages = {3--18}, publisher = {Springer Nature}, title = {{Monitorability under assumptions}}, doi = {10.1007/978-3-030-60508-7_1}, volume = {12399}, year = {2020}, } @inproceedings{8732, abstract = {A simple drawing D(G) of a graph G is one where each pair of edges share at most one point: either a common endpoint or a proper crossing. An edge e in the complement of G can be inserted into D(G) if there exists a simple drawing of G+e extending D(G). As a result of Levi’s Enlargement Lemma, if a drawing is rectilinear (pseudolinear), that is, the edges can be extended into an arrangement of lines (pseudolines), then any edge in the complement of G can be inserted. In contrast, we show that it is NP -complete to decide whether one edge can be inserted into a simple drawing. This remains true even if we assume that the drawing is pseudocircular, that is, the edges can be extended to an arrangement of pseudocircles. On the positive side, we show that, given an arrangement of pseudocircles A and a pseudosegment σ , it can be decided in polynomial time whether there exists a pseudocircle Φσ extending σ for which A∪{Φσ} is again an arrangement of pseudocircles.}, author = {Arroyo Guevara, Alan M and Klute, Fabian and Parada, Irene and Seidel, Raimund and Vogtenhuber, Birgit and Wiedera, Tilo}, booktitle = {Graph-Theoretic Concepts in Computer Science}, isbn = {9783030604394}, issn = {1611-3349}, location = {Leeds, United Kingdom}, pages = {325--338}, publisher = {Springer Nature}, title = {{Inserting one edge into a simple drawing is hard}}, doi = {10.1007/978-3-030-60440-0_26}, volume = {12301}, year = {2020}, } @inproceedings{8987, abstract = {Currently several projects aim at designing and implementing protocols for privacy preserving automated contact tracing to help fight the current pandemic. Those proposal are quite similar, and in their most basic form basically propose an app for mobile phones which broadcasts frequently changing pseudorandom identifiers via (low energy) Bluetooth, and at the same time, the app stores IDs broadcast by phones in its proximity. Only if a user is tested positive, they upload either the beacons they did broadcast (which is the case in decentralized proposals as DP-3T, east and west coast PACT or Covid watch) or received (as in Popp-PT or ROBERT) during the last two weeks or so. Vaudenay [eprint 2020/399] observes that this basic scheme (he considers the DP-3T proposal) succumbs to relay and even replay attacks, and proposes more complex interactive schemes which prevent those attacks without giving up too many privacy aspects. Unfortunately interaction is problematic for this application for efficiency and security reasons. The countermeasures that have been suggested so far are either not practical or give up on key privacy aspects. We propose a simple non-interactive variant of the basic protocol that (security) Provably prevents replay and (if location data is available) relay attacks. (privacy) The data of all parties (even jointly) reveals no information on the location or time where encounters happened. (efficiency) The broadcasted message can fit into 128 bits and uses only basic crypto (commitments and secret key authentication). Towards this end we introduce the concept of “delayed authentication”, which basically is a message authentication code where verification can be done in two steps, where the first doesn’t require the key, and the second doesn’t require the message.}, author = {Pietrzak, Krzysztof Z}, booktitle = {Progress in Cryptology}, isbn = {9783030652760}, issn = {1611-3349}, location = {Bangalore, India}, pages = {3--15}, publisher = {Springer Nature}, title = {{Delayed authentication: Preventing replay and relay attacks in private contact tracing}}, doi = {10.1007/978-3-030-65277-7_1}, volume = {12578}, year = {2020}, } @inproceedings{9299, abstract = {We call a multigraph non-homotopic if it can be drawn in the plane in such a way that no two edges connecting the same pair of vertices can be continuously transformed into each other without passing through a vertex, and no loop can be shrunk to its end-vertex in the same way. It is easy to see that a non-homotopic multigraph on n>1 vertices can have arbitrarily many edges. We prove that the number of crossings between the edges of a non-homotopic multigraph with n vertices and m>4n edges is larger than cm2n for some constant c>0 , and that this bound is tight up to a polylogarithmic factor. We also show that the lower bound is not asymptotically sharp as n is fixed and m⟶∞ .}, author = {Pach, János and Tardos, Gábor and Tóth, Géza}, booktitle = {28th International Symposium on Graph Drawing and Network Visualization}, isbn = {9783030687656}, issn = {1611-3349}, location = {Virtual, Online}, pages = {359--371}, publisher = {Springer Nature}, title = {{Crossings between non-homotopic edges}}, doi = {10.1007/978-3-030-68766-3_28}, volume = {12590}, year = {2020}, } @inproceedings{18251, abstract = {Magnetic Resonance Imaging (MRI) has long been considered to be among the gold standards of today’s diagnostic imaging. The most significant drawback of MRI is long acquisition times, prohibiting its use in standard practice for some applications. Compressed sensing (CS) proposes to subsample the k-space (the Fourier domain dual to the physical space of spatial coordinates) leading to significantly accelerated acquisition. However, the benefit of compressed sensing has not been fully exploited; most of the sampling densities obtained through CS do not produce a trajectory that obeys the stringent constraints of the MRI machine imposed in practice. Inspired by recent success of deep learning-based approaches for image reconstruction and ideas from computational imaging on learning-based design of imaging systems, we introduce 3D FLAT, a novel protocol for data-driven design of 3D non-Cartesian accelerated trajectories in MRI. Our proposal leverages the entire 3D k-space to simultaneously learn a physically feasible acquisition trajectory with a reconstruction method. Experimental results, performed as a proof-of-concept, suggest that 3D FLAT achieves higher image quality for a given readout time compared to standard trajectories such as radial, stack-of-stars, or 2D learned trajectories (trajectories that evolve only in the 2D plane while fully sampling along the third dimension). Furthermore, we demonstrate evidence supporting the significant benefit of performing MRI acquisitions using non-Cartesian 3D trajectories over 2D non-Cartesian trajectories acquired slice-wise.}, author = {Alush-Aben, Jonathan and Ackerman-Schraier, Linor and Weiss, Tomer and Vedula, Sanketh and Senouf, Ortal and Bronstein, Alexander}, booktitle = {International Workshop on Machine Learning for Medical Image Reconstruction}, isbn = {9783030615970}, issn = {1611-3349}, location = {Lima, Peru}, pages = {3 -- 16}, publisher = {Springer Nature}, title = {{3D FLAT: Feasible learned acquisition trajectories for accelerated MRI}}, doi = {10.1007/978-3-030-61598-7_1}, volume = {12450}, year = {2020}, } @inproceedings{8322, abstract = {Reverse firewalls were introduced at Eurocrypt 2015 by Miro-nov and Stephens-Davidowitz, as a method for protecting cryptographic protocols against attacks on the devices of the honest parties. In a nutshell: a reverse firewall is placed outside of a device and its goal is to “sanitize” the messages sent by it, in such a way that a malicious device cannot leak its secrets to the outside world. It is typically assumed that the cryptographic devices are attacked in a “functionality-preserving way” (i.e. informally speaking, the functionality of the protocol remains unchanged under this attacks). In their paper, Mironov and Stephens-Davidowitz construct a protocol for passively-secure two-party computations with firewalls, leaving extension of this result to stronger models as an open question. In this paper, we address this problem by constructing a protocol for secure computation with firewalls that has two main advantages over the original protocol from Eurocrypt 2015. Firstly, it is a multiparty computation protocol (i.e. it works for an arbitrary number n of the parties, and not just for 2). Secondly, it is secure in much stronger corruption settings, namely in the active corruption model. More precisely: we consider an adversary that can fully corrupt up to 𝑛−1 parties, while the remaining parties are corrupt in a functionality-preserving way. Our core techniques are: malleable commitments and malleable non-interactive zero-knowledge, which in particular allow us to create a novel protocol for multiparty augmented coin-tossing into the well with reverse firewalls (that is based on a protocol of Lindell from Crypto 2001).}, author = {Chakraborty, Suvradip and Dziembowski, Stefan and Nielsen, Jesper Buus}, booktitle = {Advances in Cryptology – CRYPTO 2020}, isbn = {9783030568795}, issn = {1611-3349}, location = {Santa Barbara, CA, United States}, pages = {732--762}, publisher = {Springer Nature}, title = {{Reverse firewalls for actively secure MPCs}}, doi = {10.1007/978-3-030-56880-1_26}, volume = {12171}, year = {2020}, } @inproceedings{8728, abstract = {Discrete-time Markov Chains (MCs) and Markov Decision Processes (MDPs) are two standard formalisms in system analysis. Their main associated quantitative objectives are hitting probabilities, discounted sum, and mean payoff. Although there are many techniques for computing these objectives in general MCs/MDPs, they have not been thoroughly studied in terms of parameterized algorithms, particularly when treewidth is used as the parameter. This is in sharp contrast to qualitative objectives for MCs, MDPs and graph games, for which treewidth-based algorithms yield significant complexity improvements. In this work, we show that treewidth can also be used to obtain faster algorithms for the quantitative problems. For an MC with n states and m transitions, we show that each of the classical quantitative objectives can be computed in O((n+m)⋅t2) time, given a tree decomposition of the MC with width t. Our results also imply a bound of O(κ⋅(n+m)⋅t2) for each objective on MDPs, where κ is the number of strategy-iteration refinements required for the given input and objective. Finally, we make an experimental evaluation of our new algorithms on low-treewidth MCs and MDPs obtained from the DaCapo benchmark suite. Our experiments show that on low-treewidth MCs and MDPs, our algorithms outperform existing well-established methods by one or more orders of magnitude.}, author = {Asadi, Ali and Chatterjee, Krishnendu and Goharshady, Amir Kafshdar and Mohammadi, Kiarash and Pavlogiannis, Andreas}, booktitle = {Automated Technology for Verification and Analysis}, isbn = {9783030591519}, issn = {1611-3349}, location = {Hanoi, Vietnam}, pages = {253--270}, publisher = {Springer Nature}, title = {{Faster algorithms for quantitative analysis of MCs and MDPs with small treewidth}}, doi = {10.1007/978-3-030-59152-6_14}, volume = {12302}, year = {2020}, } @inproceedings{7810, abstract = {Interprocedural data-flow analyses form an expressive and useful paradigm of numerous static analysis applications, such as live variables analysis, alias analysis and null pointers analysis. The most widely-used framework for interprocedural data-flow analysis is IFDS, which encompasses distributive data-flow functions over a finite domain. On-demand data-flow analyses restrict the focus of the analysis on specific program locations and data facts. This setting provides a natural split between (i) an offline (or preprocessing) phase, where the program is partially analyzed and analysis summaries are created, and (ii) an online (or query) phase, where analysis queries arrive on demand and the summaries are used to speed up answering queries. In this work, we consider on-demand IFDS analyses where the queries concern program locations of the same procedure (aka same-context queries). We exploit the fact that flow graphs of programs have low treewidth to develop faster algorithms that are space and time optimal for many common data-flow analyses, in both the preprocessing and the query phase. We also use treewidth to develop query solutions that are embarrassingly parallelizable, i.e. the total work for answering each query is split to a number of threads such that each thread performs only a constant amount of work. Finally, we implement a static analyzer based on our algorithms, and perform a series of on-demand analysis experiments on standard benchmarks. Our experimental results show a drastic speed-up of the queries after only a lightweight preprocessing phase, which significantly outperforms existing techniques.}, author = {Chatterjee, Krishnendu and Goharshady, Amir Kafshdar and Ibsen-Jensen, Rasmus and Pavlogiannis, Andreas}, booktitle = {European Symposium on Programming}, isbn = {9783030449131}, issn = {1611-3349}, location = {Dublin, Ireland}, pages = {112--140}, publisher = {Springer Nature}, title = {{Optimal and perfectly parallel algorithms for on-demand data-flow analysis}}, doi = {10.1007/978-3-030-44914-8_5}, volume = {12075}, year = {2020}, } @inproceedings{6163, abstract = {We propose a new non-orthogonal basis to express the 3D Euclidean space in terms of a regular grid. Every grid point, each represented by integer 3-coordinates, corresponds to rhombic dodecahedron centroid. Rhombic dodecahedron is a space filling polyhedron which represents the close packing of spheres in 3D space and the Voronoi structures of the face centered cubic (FCC) lattice. In order to illustrate the interest of the new coordinate system, we propose the characterization of 3D digital plane with its topological features, such as the interrelation between the thickness of the digital plane and the separability constraint we aim to obtain. A characterization of a 3D digital sphere with relevant topological features is proposed as well with the help of a 48 symmetry that comes with the new coordinate system.}, author = {Biswas, Ranita and Largeteau-Skapin, Gaëlle and Zrour, Rita and Andres, Eric}, booktitle = {21st IAPR International Conference on Discrete Geometry for Computer Imagery}, isbn = {978-3-6624-6446-5}, issn = {0302-9743}, location = {Marne-la-Vallée, France}, pages = {27--37}, publisher = {Springer Berlin Heidelberg}, title = {{Rhombic dodecahedron grid—coordinate system and 3D digital object definitions}}, doi = {10.1007/978-3-030-14085-4_3}, volume = {11414}, year = {2019}, } @inproceedings{6430, abstract = {A proxy re-encryption (PRE) scheme is a public-key encryption scheme that allows the holder of a key pk to derive a re-encryption key for any other key 𝑝𝑘′. This re-encryption key lets anyone transform ciphertexts under pk into ciphertexts under 𝑝𝑘′ without having to know the underlying message, while transformations from 𝑝𝑘′ to pk should not be possible (unidirectional). Security is defined in a multi-user setting against an adversary that gets the users’ public keys and can ask for re-encryption keys and can corrupt users by requesting their secret keys. Any ciphertext that the adversary cannot trivially decrypt given the obtained secret and re-encryption keys should be secure. All existing security proofs for PRE only show selective security, where the adversary must first declare the users it wants to corrupt. This can be lifted to more meaningful adaptive security by guessing the set of corrupted users among the n users, which loses a factor exponential in Open image in new window , rendering the result meaningless already for moderate Open image in new window . Jafargholi et al. (CRYPTO’17) proposed a framework that in some cases allows to give adaptive security proofs for schemes which were previously only known to be selectively secure, while avoiding the exponential loss that results from guessing the adaptive choices made by an adversary. We apply their framework to PREs that satisfy some natural additional properties. Concretely, we give a more fine-grained reduction for several unidirectional PREs, proving adaptive security at a much smaller loss. The loss depends on the graph of users whose edges represent the re-encryption keys queried by the adversary. For trees and chains the loss is quasi-polynomial in the size and for general graphs it is exponential in their depth and indegree (instead of their size as for previous reductions). Fortunately, trees and low-depth graphs cover many, if not most, interesting applications. Our results apply e.g. to the bilinear-map based PRE schemes by Ateniese et al. (NDSS’05 and CT-RSA’09), Gentry’s FHE-based scheme (STOC’09) and the LWE-based scheme by Chandran et al. (PKC’14).}, author = {Fuchsbauer, Georg and Kamath Hosdurg, Chethan and Klein, Karen and Pietrzak, Krzysztof Z}, isbn = {9783030172589}, issn = {1611-3349}, location = {Beijing, China}, pages = {317--346}, publisher = {Springer Nature}, title = {{Adaptively secure proxy re-encryption}}, doi = {10.1007/978-3-030-17259-6_11}, volume = {11443}, year = {2019}, } @inproceedings{6462, abstract = {A controller is a device that interacts with a plant. At each time point,it reads the plant’s state and issues commands with the goal that the plant oper-ates optimally. Constructing optimal controllers is a fundamental and challengingproblem. Machine learning techniques have recently been successfully applied totrain controllers, yet they have limitations. Learned controllers are monolithic andhard to reason about. In particular, it is difficult to add features without retraining,to guarantee any level of performance, and to achieve acceptable performancewhen encountering untrained scenarios. These limitations can be addressed bydeploying quantitative run-timeshieldsthat serve as a proxy for the controller.At each time point, the shield reads the command issued by the controller andmay choose to alter it before passing it on to the plant. We show how optimalshields that interfere as little as possible while guaranteeing a desired level ofcontroller performance, can be generated systematically and automatically usingreactive synthesis. First, we abstract the plant by building a stochastic model.Second, we consider the learned controller to be a black box. Third, we mea-surecontroller performanceandshield interferenceby two quantitative run-timemeasures that are formally defined using weighted automata. Then, the problemof constructing a shield that guarantees maximal performance with minimal inter-ference is the problem of finding an optimal strategy in a stochastic2-player game“controller versus shield” played on the abstract state space of the plant with aquantitative objective obtained from combining the performance and interferencemeasures. We illustrate the effectiveness of our approach by automatically con-structing lightweight shields for learned traffic-light controllers in various roadnetworks. The shields we generate avoid liveness bugs, improve controller per-formance in untrained and changing traffic situations, and add features to learnedcontrollers, such as giving priority to emergency vehicles.}, author = {Avni, Guy and Bloem, Roderick and Chatterjee, Krishnendu and Henzinger, Thomas A and Konighofer, Bettina and Pranger, Stefan}, booktitle = {31st International Conference on Computer-Aided Verification}, isbn = {9783030255398}, issn = {0302-9743}, location = {New York, NY, United States}, pages = {630--649}, publisher = {Springer}, title = {{Run-time optimization for learned controllers through quantitative games}}, doi = {10.1007/978-3-030-25540-4_36}, volume = {11561}, year = {2019}, } @inproceedings{6482, abstract = {Computer vision systems for automatic image categorization have become accurate and reliable enough that they can run continuously for days or even years as components of real-world commercial applications. A major open problem in this context, however, is quality control. Good classification performance can only be expected if systems run under the specific conditions, in particular data distributions, that they were trained for. Surprisingly, none of the currently used deep network architectures have a built-in functionality that could detect if a network operates on data from a distribution it was not trained for, such that potentially a warning to the human users could be triggered. In this work, we describe KS(conf), a procedure for detecting such outside of specifications (out-of-specs) operation, based on statistical testing of the network outputs. We show by extensive experiments using the ImageNet, AwA2 and DAVIS datasets on a variety of ConvNets architectures that KS(conf) reliably detects out-of-specs situations. It furthermore has a number of properties that make it a promising candidate for practical deployment: it is easy to implement, adds almost no overhead to the system, works with all networks, including pretrained ones, and requires no a priori knowledge of how the data distribution could change. }, author = {Sun, Rémy and Lampert, Christoph}, isbn = {9783030129385}, issn = {1611-3349}, location = {Stuttgart, Germany}, pages = {244--259}, publisher = {Springer Nature}, title = {{KS(conf): A light-weight test if a ConvNet operates outside of Its specifications}}, doi = {10.1007/978-3-030-12939-2_18}, volume = {11269}, year = {2019}, } @inproceedings{6493, abstract = {We present two algorithmic approaches for synthesizing linear hybrid automata from experimental data. Unlike previous approaches, our algorithms work without a template and generate an automaton with nondeterministic guards and invariants, and with an arbitrary number and topology of modes. They thus construct a succinct model from the data and provide formal guarantees. In particular, (1) the generated automaton can reproduce the data up to a specified tolerance and (2) the automaton is tight, given the first guarantee. Our first approach encodes the synthesis problem as a logical formula in the theory of linear arithmetic, which can then be solved by an SMT solver. This approach minimizes the number of modes in the resulting model but is only feasible for limited data sets. To address scalability, we propose a second approach that does not enforce to find a minimal model. The algorithm constructs an initial automaton and then iteratively extends the automaton based on processing new data. Therefore the algorithm is well-suited for online and synthesis-in-the-loop applications. The core of the algorithm is a membership query that checks whether, within the specified tolerance, a given data set can result from the execution of a given automaton. We solve this membership problem for linear hybrid automata by repeated reachability computations. We demonstrate the effectiveness of the algorithm on synthetic data sets and on cardiac-cell measurements.}, author = {Garcia Soto, Miriam and Henzinger, Thomas A and Schilling, Christian and Zeleznik, Luka}, booktitle = {31st International Conference on Computer-Aided Verification}, isbn = {9783030255398}, issn = {0302-9743}, keywords = {Synthesis, Linear hybrid automaton, Membership}, location = {New York City, NY, USA}, pages = {297--314}, publisher = {Springer}, title = {{Membership-based synthesis of linear hybrid automata}}, doi = {10.1007/978-3-030-25540-4_16}, volume = {11561}, year = {2019}, } @inbook{6726, abstract = {Randomness is an essential part of any secure cryptosystem, but many constructions rely on distributions that are not uniform. This is particularly true for lattice based cryptosystems, which more often than not make use of discrete Gaussian distributions over the integers. For practical purposes it is crucial to evaluate the impact that approximation errors have on the security of a scheme to provide the best possible trade-off between security and performance. Recent years have seen surprising results allowing to use relatively low precision while maintaining high levels of security. A key insight in these results is that sampling a distribution with low relative error can provide very strong security guarantees. Since floating point numbers provide guarantees on the relative approximation error, they seem a suitable tool in this setting, but it is not obvious which sampling algorithms can actually profit from them. While previous works have shown that inversion sampling can be adapted to provide a low relative error (Pöppelmann et al., CHES 2014; Prest, ASIACRYPT 2017), other works have called into question if this is possible for other sampling techniques (Zheng et al., Eprint report 2018/309). In this work, we consider all sampling algorithms that are popular in the cryptographic setting and analyze the relationship of floating point precision and the resulting relative error. We show that all of the algorithms either natively achieve a low relative error or can be adapted to do so.}, author = {Walter, Michael}, booktitle = {Progress in Cryptology – AFRICACRYPT 2019}, editor = {Buchmann, J and Nitaj, A and Rachidi, T}, isbn = {978-3-0302-3695-3}, issn = {1611-3349}, location = {Rabat, Morocco}, pages = {157--180}, publisher = {Springer Nature}, title = {{Sampling the integers with low relative error}}, doi = {10.1007/978-3-030-23696-0_9}, volume = {11627}, year = {2019}, } @inproceedings{6942, abstract = {Graph games and Markov decision processes (MDPs) are standard models in reactive synthesis and verification of probabilistic systems with nondeterminism. The class of 𝜔 -regular winning conditions; e.g., safety, reachability, liveness, parity conditions; provides a robust and expressive specification formalism for properties that arise in analysis of reactive systems. The resolutions of nondeterminism in games and MDPs are represented as strategies, and we consider succinct representation of such strategies. The decision-tree data structure from machine learning retains the flavor of decisions of strategies and allows entropy-based minimization to obtain succinct trees. However, in contrast to traditional machine-learning problems where small errors are allowed, for winning strategies in graph games and MDPs no error is allowed, and the decision tree must represent the entire strategy. In this work we propose decision trees with linear classifiers for representation of strategies in graph games and MDPs. We have implemented strategy representation using this data structure and we present experimental results for problems on graph games and MDPs, which show that this new data structure presents a much more efficient strategy representation as compared to standard decision trees.}, author = {Ashok, Pranav and Brázdil, Tomáš and Chatterjee, Krishnendu and Křetínský, Jan and Lampert, Christoph and Toman, Viktor}, booktitle = {16th International Conference on Quantitative Evaluation of Systems}, isbn = {9783030302801}, issn = {0302-9743}, location = {Glasgow, United Kingdom}, pages = {109--128}, publisher = {Springer Nature}, title = {{Strategy representation by decision trees with linear classifiers}}, doi = {10.1007/978-3-030-30281-8_7}, volume = {11785}, year = {2019}, } @inproceedings{7147, abstract = {The expression of a gene is characterised by its transcription factors and the function processing them. If the transcription factors are not affected by gene products, the regulating function is often represented as a combinational logic circuit, where the outputs (product) are determined by current input values (transcription factors) only, and are hence independent on their relative arrival times. However, the simultaneous arrival of transcription factors (TFs) in genetic circuits is a strong assumption, given that the processes of transcription and translation of a gene into a protein introduce intrinsic time delays and that there is no global synchronisation among the arrival times of different molecular species at molecular targets. In this paper, we construct an experimentally implementable genetic circuit with two inputs and a single output, such that, in presence of small delays in input arrival, the circuit exhibits qualitatively distinct observable phenotypes. In particular, these phenotypes are long lived transients: they all converge to a single value, but so slowly, that they seem stable for an extended time period, longer than typical experiment duration. We used rule-based language to prototype our circuit, and we implemented a search for finding the parameter combinations raising the phenotypes of interest. The behaviour of our prototype circuit has wide implications. First, it suggests that GRNs can exploit event timing to create phenotypes. Second, it opens the possibility that GRNs are using event timing to react to stimuli and memorise events, without explicit feedback in regulation. From the modelling perspective, our prototype circuit demonstrates the critical importance of analysing the transient dynamics at the promoter binding sites of the DNA, before applying rapid equilibrium assumptions.}, author = {Guet, Calin C and Henzinger, Thomas A and Igler, Claudia and Petrov, Tatjana and Sezgin, Ali}, booktitle = {17th International Conference on Computational Methods in Systems Biology}, isbn = {9783030313036}, issn = {1611-3349}, location = {Trieste, Italy}, pages = {155--187}, publisher = {Springer Nature}, title = {{Transient memory in gene regulation}}, doi = {10.1007/978-3-030-31304-3_9}, volume = {11773}, year = {2019}, } @inproceedings{7159, abstract = {Cyber-physical systems (CPS) and the Internet-of-Things (IoT) result in a tremendous amount of generated, measured and recorded time-series data. Extracting temporal segments that encode patterns with useful information out of these huge amounts of data is an extremely difficult problem. We propose shape expressions as a declarative formalism for specifying, querying and extracting sophisticated temporal patterns from possibly noisy data. Shape expressions are regular expressions with arbitrary (linear, exponential, sinusoidal, etc.) shapes with parameters as atomic predicates and additional constraints on these parameters. We equip shape expressions with a novel noisy semantics that combines regular expression matching semantics with statistical regression. We characterize essential properties of the formalism and propose an efficient approximate shape expression matching procedure. We demonstrate the wide applicability of this technique on two case studies. }, author = {Ničković, Dejan and Qin, Xin and Ferrere, Thomas and Mateis, Cristinel and Deshmukh, Jyotirmoy}, booktitle = {19th International Conference on Runtime Verification}, isbn = {9783030320782}, issn = {0302-9743}, location = {Porto, Portugal}, pages = {292--309}, publisher = {Springer Nature}, title = {{Shape expressions for specifying and extracting signal features}}, doi = {10.1007/978-3-030-32079-9_17}, volume = {11757}, year = {2019}, } @inproceedings{7183, abstract = {A probabilistic vector addition system with states (pVASS) is a finite state Markov process augmented with non-negative integer counters that can be incremented or decremented during each state transition, blocking any behaviour that would cause a counter to decrease below zero. The pVASS can be used as abstractions of probabilistic programs with many decidable properties. The use of pVASS as abstractions requires the presence of nondeterminism in the model. In this paper, we develop techniques for checking fast termination of pVASS with nondeterminism. That is, for every initial configuration of size n, we consider the worst expected number of transitions needed to reach a configuration with some counter negative (the expected termination time). We show that the problem whether the asymptotic expected termination time is linear is decidable in polynomial time for a certain natural class of pVASS with nondeterminism. Furthermore, we show the following dichotomy: if the asymptotic expected termination time is not linear, then it is at least quadratic, i.e., in Ω(n2).}, author = {Brázdil, Tomás and Chatterjee, Krishnendu and Kucera, Antonín and Novotný, Petr and Velan, Dominik}, booktitle = {International Symposium on Automated Technology for Verification and Analysis}, isbn = {9783030317836}, issn = {1611-3349}, location = {Taipei, Taiwan}, pages = {462--478}, publisher = {Springer Nature}, title = {{Deciding fast termination for probabilistic VASS with nondeterminism}}, doi = {10.1007/978-3-030-31784-3_27}, volume = {11781}, year = {2019}, } @inproceedings{7228, abstract = {Traditional concurrent programming involves manipulating shared mutable state. Alternatives to this programming style are communicating sequential processes (CSP) and actor models, which share data via explicit communication. These models have been known for almost half a century, and have recently had started to gain significant traction among modern programming languages. The common abstraction for communication between several processes is the channel. Although channels are similar to producer-consumer data structures, they have different semantics and support additional operations, such as the select expression. Despite their growing popularity, most known implementations of channels use lock-based data structures and can be rather inefficient. In this paper, we present the first efficient lock-free algorithm for implementing a communication channel for CSP programming. We provide implementations and experimental results in the Kotlin and Go programming languages. Our new algorithm outperforms existing implementations on many workloads, while providing non-blocking progress guarantee. Our design can serve as an example of how to construct general communication data structures for CSP and actor models. }, author = {Koval, Nikita and Alistarh, Dan-Adrian and Elizarov, Roman}, booktitle = {25th Anniversary of Euro-Par}, isbn = {978-3-0302-9399-4}, issn = {1611-3349}, location = {Göttingen, Germany}, pages = {317--333}, publisher = {Springer Nature}, title = {{Scalable FIFO channels for programming via communicating sequential processes}}, doi = {10.1007/978-3-030-29400-7_23}, volume = {11725}, year = {2019}, } @inproceedings{7230, abstract = {Simple drawings of graphs are those in which each pair of edges share at most one point, either a common endpoint or a proper crossing. In this paper we study the problem of extending a simple drawing D(G) of a graph G by inserting a set of edges from the complement of G into D(G) such that the result is a simple drawing. In the context of rectilinear drawings, the problem is trivial. For pseudolinear drawings, the existence of such an extension follows from Levi’s enlargement lemma. In contrast, we prove that deciding if a given set of edges can be inserted into a simple drawing is NP-complete. Moreover, we show that the maximization version of the problem is APX-hard. We also present a polynomial-time algorithm for deciding whether one edge uv can be inserted into D(G) when {u,v} is a dominating set for the graph G.}, author = {Arroyo Guevara, Alan M and Derka, Martin and Parada, Irene}, booktitle = {27th International Symposium on Graph Drawing and Network Visualization}, isbn = {978-3-0303-5801-3}, issn = {1611-3349}, location = {Prague, Czech Republic}, pages = {230--243}, publisher = {Springer Nature}, title = {{Extending simple drawings}}, doi = {10.1007/978-3-030-35802-0_18}, volume = {11904}, year = {2019}, }