@inproceedings{1134, abstract = {Hybrid systems have both continuous and discrete dynamics and are useful for modeling a variety of control systems, from air traffic control protocols to robotic maneuvers and beyond. Recently, numerous powerful and scalable tools for analyzing hybrid systems have emerged. Several of these tools implement automated formal methods for mathematically proving a system meets a specification. This tutorial session will present three recent hybrid systems tools: C2E2, HyST, and TuLiP. C2E2 is a simulated-based verification tool for hybrid systems, and uses validated numerical solvers and bloating of simulation traces to verify systems meet specifications. HyST is a hybrid systems model transformation and translation tool, and uses a canonical intermediate representation to support most of the recent verification tools, as well as automated sound abstractions that simplify verification of a given hybrid system. TuLiP is a controller synthesis tool for hybrid systems, where given a temporal logic specification to be satisfied for a system (plant) model, TuLiP will find a controller that meets a given specification. © 2016 IEEE.}, author = {Duggirala, Parasara and Fan, Chuchu and Potok, Matthew and Qi, Bolun and Mitra, Sayan and Viswanathan, Mahesh and Bak, Stanley and Bogomolov, Sergiy and Johnson, Taylor and Nguyen, Luan and Schilling, Christian and Sogokon, Andrew and Tran, Hoang and Xiang, Weiming}, booktitle = {2016 IEEE Conference on Control Applications}, location = {Buenos Aires, Argentina }, publisher = {IEEE}, title = {{Tutorial: Software tools for hybrid systems verification transformation and synthesis C2E2 HyST and TuLiP}}, doi = {10.1109/CCA.2016.7587948}, year = {2016}, } @inproceedings{1136, abstract = {We propose an interactive sculpting system for seamlessly editing pre-computed animations of liquid, without the need for any resimulation. The input is a sequence of meshes without correspondences representing the liquid surface over time. Our method enables the efficient selection of consistent space-time parts of this animation, such as moving waves or droplets, which we call space-time features. Once selected, a feature can be copied, edited, or duplicated and then pasted back anywhere in space and time in the same or in another liquid animation sequence. Our method circumvents tedious user interactions by automatically computing the spatial and temporal ranges of the selected feature. We also provide space-time shape editing tools for non-uniform scaling, rotation, trajectory changes, and temporal editing to locally speed up or slow down motion. Using our tools, the user can edit and progressively refine any input simulation result, possibly using a library of precomputed space-time features extracted from other animations. In contrast to the trial-and-error loop usually required to edit animation results through the tuning of indirect simulation parameters, our method gives the user full control over the edited space-time behaviors. © 2016 Copyright held by the owner/author(s).}, author = {Manteaux, Pierre and Vimont, Ulysse and Wojtan, Christopher J and Rohmer, Damien and Cani, Marie}, booktitle = {Proceedings of the 9th International Conference on Motion in Games }, location = {San Francisco, CA, USA}, publisher = {ACM}, title = {{Space-time sculpting of liquid animation}}, doi = {10.1145/2994258.2994261}, year = {2016}, } @article{1137, abstract = {RASGRP1 is an important guanine nucleotide exchange factor and activator of the RAS-MAPK pathway following T cell antigen receptor (TCR) signaling. The consequences of RASGRP1 mutations in humans are unknown. In a patient with recurrent bacterial and viral infections, born to healthy consanguineous parents, we used homozygosity mapping and exome sequencing to identify a biallelic stop-gain variant in RASGRP1. This variant segregated perfectly with the disease and has not been reported in genetic databases. RASGRP1 deficiency was associated in T cells and B cells with decreased phosphorylation of the extracellular-signal-regulated serine kinase ERK, which was restored following expression of wild-type RASGRP1. RASGRP1 deficiency also resulted in defective proliferation, activation and motility of T cells and B cells. RASGRP1-deficient natural killer (NK) cells exhibited impaired cytotoxicity with defective granule convergence and actin accumulation. Interaction proteomics identified the dynein light chain DYNLL1 as interacting with RASGRP1, which links RASGRP1 to cytoskeletal dynamics. RASGRP1-deficient cells showed decreased activation of the GTPase RhoA. Treatment with lenalidomide increased RhoA activity and reversed the migration and activation defects of RASGRP1-deficient lymphocytes.}, author = {Salzer, Elisabeth and Çaǧdaş, Deniz and Hons, Miroslav and Mace, Emily and Garncarz, Wojciech and Petronczki, Oezlem and Platzer, René and Pfajfer, Laurène and Bilic, Ivan and Ban, Sol and Willmann, Katharina and Mukherjee, Malini and Supper, Verena and Hsu, Hsiangting and Banerjee, Pinaki and Sinha, Papiya and Mcclanahan, Fabienne and Zlabinger, Gerhard and Pickl, Winfried and Gribben, John and Stockinger, Hannes and Bennett, Keiryn and Huppa, Johannes and Dupré, Loï̈C and Sanal, Özden and Jäger, Ulrich and Sixt, Michael K and Tezcan, Ilhan and Orange, Jordan and Boztug, Kaan}, journal = {Nature Immunology}, number = {12}, pages = {1352 -- 1360}, publisher = {Nature Publishing Group}, title = {{RASGRP1 deficiency causes immunodeficiency with impaired cytoskeletal dynamics}}, doi = {10.1038/ni.3575}, volume = {17}, year = {2016}, } @inproceedings{1138, abstract = {Automata with monitor counters, where the transitions do not depend on counter values, and nested weighted automata are two expressive automata-theoretic frameworks for quantitative properties. For a well-studied and wide class of quantitative functions, we establish that automata with monitor counters and nested weighted automata are equivalent. We study for the first time such quantitative automata under probabilistic semantics. We show that several problems that are undecidable for the classical questions of emptiness and universality become decidable under the probabilistic semantics. We present a complete picture of decidability for such automata, and even an almost-complete picture of computational complexity, for the probabilistic questions we consider. © 2016 ACM.}, author = {Chatterjee, Krishnendu and Henzinger, Thomas A and Otop, Jan}, booktitle = {Proceedings of the 31st Annual ACM/IEEE Symposium}, location = {New York, NY, USA}, pages = {76 -- 85}, publisher = {IEEE}, title = {{Quantitative automata under probabilistic semantics}}, doi = {10.1145/2933575.2933588}, year = {2016}, } @inproceedings{1140, abstract = {Given a model of a system and an objective, the model-checking question asks whether the model satisfies the objective. We study polynomial-time problems in two classical models, graphs and Markov Decision Processes (MDPs), with respect to several fundamental -regular objectives, e.g., Rabin and Streett objectives. For many of these problems the best-known upper bounds are quadratic or cubic, yet no super-linear lower bounds are known. In this work our contributions are two-fold: First, we present several improved algorithms, and second, we present the first conditional super-linear lower bounds based on widely believed assumptions about the complexity of CNF-SAT and combinatorial Boolean matrix multiplication. A separation result for two models with respect to an objective means a conditional lower bound for one model that is strictly higher than the existing upper bound for the other model, and similarly for two objectives with respect to a model. Our results establish the following separation results: (1) A separation of models (graphs and MDPs) for disjunctive queries of reachability and Büchi objectives. (2) Two kinds of separations of objectives, both for graphs and MDPs, namely, (2a) the separation of dual objectives such as Streett/Rabin objectives, and (2b) the separation of conjunction and disjunction of multiple objectives of the same type such as safety, Büchi, and coBüchi. In summary, our results establish the first model and objective separation results for graphs and MDPs for various classical -regular objectives. Quite strikingly, we establish conditional lower bounds for the disjunction of objectives that are strictly higher than the existing upper bounds for the conjunction of the same objectives. © 2016 ACM.}, author = {Chatterjee, Krishnendu and Dvoák, Wolfgang and Henzinger, Monika H and Loitzenbauer, Veronika}, booktitle = {Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science}, location = {New York, NY, USA}, pages = {197 -- 206}, publisher = {IEEE}, title = {{Model and objective separation with conditional lower bounds: disjunction is harder than conjunction}}, doi = {10.1145/2933575.2935304}, year = {2016}, }