[{"date_updated":"2021-01-12T06:48:32Z","date_created":"2018-12-11T11:50:20Z","oa_version":"None","author":[{"full_name":"Duggirala, Parasara","first_name":"Parasara","last_name":"Duggirala"},{"last_name":"Fan","first_name":"Chuchu","full_name":"Fan, Chuchu"},{"last_name":"Potok","first_name":"Matthew","full_name":"Potok, Matthew"},{"last_name":"Qi","first_name":"Bolun","full_name":"Qi, Bolun"},{"full_name":"Mitra, Sayan","first_name":"Sayan","last_name":"Mitra"},{"full_name":"Viswanathan, Mahesh","first_name":"Mahesh","last_name":"Viswanathan"},{"last_name":"Bak","first_name":"Stanley","full_name":"Bak, Stanley"},{"full_name":"Bogomolov, Sergiy","orcid":"0000-0002-0686-0365","id":"369D9A44-F248-11E8-B48F-1D18A9856A87","last_name":"Bogomolov","first_name":"Sergiy"},{"last_name":"Johnson","first_name":"Taylor","full_name":"Johnson, Taylor"},{"full_name":"Nguyen, Luan","last_name":"Nguyen","first_name":"Luan"},{"full_name":"Schilling, Christian","first_name":"Christian","last_name":"Schilling","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-3658-1065"},{"full_name":"Sogokon, Andrew","first_name":"Andrew","last_name":"Sogokon"},{"full_name":"Tran, Hoang","first_name":"Hoang","last_name":"Tran"},{"full_name":"Xiang, Weiming","last_name":"Xiang","first_name":"Weiming"}],"publication_status":"published","title":"Tutorial: Software tools for hybrid systems verification transformation and synthesis C2E2 HyST and TuLiP","status":"public","department":[{"_id":"ToHe"}],"publisher":"IEEE","_id":"1134","year":"2016","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","abstract":[{"text":"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.","lang":"eng"}],"publist_id":"6224","article_number":"7587948","type":"conference","language":[{"iso":"eng"}],"conference":{"start_date":"2016-09-19","location":"Buenos Aires, Argentina ","end_date":"2016-09-22","name":"CCA: Control Applications "},"date_published":"2016-10-10T00:00:00Z","doi":"10.1109/CCA.2016.7587948","quality_controlled":"1","publication":"2016 IEEE Conference on Control Applications","citation":{"ieee":"P. Duggirala et al., “Tutorial: Software tools for hybrid systems verification transformation and synthesis C2E2 HyST and TuLiP,” in 2016 IEEE Conference on Control Applications, Buenos Aires, Argentina , 2016.","apa":"Duggirala, P., Fan, C., Potok, M., Qi, B., Mitra, S., Viswanathan, M., … Xiang, W. (2016). Tutorial: Software tools for hybrid systems verification transformation and synthesis C2E2 HyST and TuLiP. In 2016 IEEE Conference on Control Applications. Buenos Aires, Argentina : IEEE. https://doi.org/10.1109/CCA.2016.7587948","ista":"Duggirala P, Fan C, Potok M, Qi B, Mitra S, Viswanathan M, Bak S, Bogomolov S, Johnson T, Nguyen L, Schilling C, Sogokon A, Tran H, Xiang W. 2016. Tutorial: Software tools for hybrid systems verification transformation and synthesis C2E2 HyST and TuLiP. 2016 IEEE Conference on Control Applications. CCA: Control Applications , 7587948.","ama":"Duggirala P, Fan C, Potok M, et al. Tutorial: Software tools for hybrid systems verification transformation and synthesis C2E2 HyST and TuLiP. In: 2016 IEEE Conference on Control Applications. IEEE; 2016. doi:10.1109/CCA.2016.7587948","chicago":"Duggirala, Parasara, Chuchu Fan, Matthew Potok, Bolun Qi, Sayan Mitra, Mahesh Viswanathan, Stanley Bak, et al. “Tutorial: Software Tools for Hybrid Systems Verification Transformation and Synthesis C2E2 HyST and TuLiP.” In 2016 IEEE Conference on Control Applications. IEEE, 2016. https://doi.org/10.1109/CCA.2016.7587948.","short":"P. Duggirala, C. Fan, M. Potok, B. Qi, S. Mitra, M. Viswanathan, S. Bak, S. Bogomolov, T. Johnson, L. Nguyen, C. Schilling, A. Sogokon, H. Tran, W. Xiang, in:, 2016 IEEE Conference on Control Applications, IEEE, 2016.","mla":"Duggirala, Parasara, et al. “Tutorial: Software Tools for Hybrid Systems Verification Transformation and Synthesis C2E2 HyST and TuLiP.” 2016 IEEE Conference on Control Applications, 7587948, IEEE, 2016, doi:10.1109/CCA.2016.7587948."},"day":"10","month":"10","scopus_import":1},{"month":"10","language":[{"iso":"eng"}],"doi":"10.1145/2994258.2994261","conference":{"location":"San Francisco, CA, USA","start_date":"2016-10-10","end_date":"2016-10-12","name":"MIG: Motion in Games"},"project":[{"grant_number":"638176","_id":"2533E772-B435-11E9-9278-68D0E5697425","name":"Efficient Simulation of Natural Phenomena at Extremely Large Scales","call_identifier":"H2020"}],"quality_controlled":"1","main_file_link":[{"open_access":"1","url":"https://hal.inria.fr/hal-01367181"}],"oa":1,"ec_funded":1,"publist_id":"6222","article_number":"2994261","date_updated":"2023-02-21T09:49:49Z","date_created":"2018-12-11T11:50:20Z","author":[{"last_name":"Manteaux","first_name":"Pierre","full_name":"Manteaux, Pierre"},{"full_name":"Vimont, Ulysse","last_name":"Vimont","first_name":"Ulysse"},{"last_name":"Wojtan","first_name":"Christopher J","orcid":"0000-0001-6646-5546","id":"3C61F1D2-F248-11E8-B48F-1D18A9856A87","full_name":"Wojtan, Christopher J"},{"full_name":"Rohmer, Damien","first_name":"Damien","last_name":"Rohmer"},{"last_name":"Cani","first_name":"Marie","full_name":"Cani, Marie"}],"department":[{"_id":"ChWo"}],"publisher":"ACM","publication_status":"published","acknowledgement":"This work was partly supported by the starting grant BigSplash, as well as the advanced grant EXPRESSIVE from the European Research Council (ERC-2014-StG 638176 , and ERC-2011-ADG 20110209).","year":"2016","article_processing_charge":"No","has_accepted_license":"1","day":"10","scopus_import":"1","date_published":"2016-10-10T00:00:00Z","citation":{"chicago":"Manteaux, Pierre, Ulysse Vimont, Chris Wojtan, Damien Rohmer, and Marie Cani. “Space-Time Sculpting of Liquid Animation.” In Proceedings of the 9th International Conference on Motion in Games . ACM, 2016. https://doi.org/10.1145/2994258.2994261.","short":"P. Manteaux, U. Vimont, C. Wojtan, D. Rohmer, M. Cani, in:, Proceedings of the 9th International Conference on Motion in Games , ACM, 2016.","mla":"Manteaux, Pierre, et al. “Space-Time Sculpting of Liquid Animation.” Proceedings of the 9th International Conference on Motion in Games , 2994261, ACM, 2016, doi:10.1145/2994258.2994261.","apa":"Manteaux, P., Vimont, U., Wojtan, C., Rohmer, D., & Cani, M. (2016). Space-time sculpting of liquid animation. In Proceedings of the 9th International Conference on Motion in Games . San Francisco, CA, USA: ACM. https://doi.org/10.1145/2994258.2994261","ieee":"P. Manteaux, U. Vimont, C. Wojtan, D. Rohmer, and M. Cani, “Space-time sculpting of liquid animation,” in Proceedings of the 9th International Conference on Motion in Games , San Francisco, CA, USA, 2016.","ista":"Manteaux P, Vimont U, Wojtan C, Rohmer D, Cani M. 2016. Space-time sculpting of liquid animation. Proceedings of the 9th International Conference on Motion in Games . MIG: Motion in Games, 2994261.","ama":"Manteaux P, Vimont U, Wojtan C, Rohmer D, Cani M. Space-time sculpting of liquid animation. In: Proceedings of the 9th International Conference on Motion in Games . ACM; 2016. doi:10.1145/2994258.2994261"},"publication":"Proceedings of the 9th International Conference on Motion in Games ","abstract":[{"text":"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).","lang":"eng"}],"type":"conference","oa_version":"Submitted Version","ddc":["004"],"status":"public","title":"Space-time sculpting of liquid animation","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"1136"},{"scopus_import":1,"day":"01","article_processing_charge":"No","publication":"Nature Immunology","citation":{"ama":"Salzer E, Çaǧdaş D, Hons M, et al. RASGRP1 deficiency causes immunodeficiency with impaired cytoskeletal dynamics. Nature Immunology. 2016;17(12):1352-1360. doi:10.1038/ni.3575","ista":"Salzer E, Çaǧdaş D, Hons M, Mace E, Garncarz W, Petronczki O, Platzer R, Pfajfer L, Bilic I, Ban S, Willmann K, Mukherjee M, Supper V, Hsu H, Banerjee P, Sinha P, Mcclanahan F, Zlabinger G, Pickl W, Gribben J, Stockinger H, Bennett K, Huppa J, Dupré L, Sanal Ö, Jäger U, Sixt MK, Tezcan I, Orange J, Boztug K. 2016. RASGRP1 deficiency causes immunodeficiency with impaired cytoskeletal dynamics. Nature Immunology. 17(12), 1352–1360.","ieee":"E. Salzer et al., “RASGRP1 deficiency causes immunodeficiency with impaired cytoskeletal dynamics,” Nature Immunology, vol. 17, no. 12. Nature Publishing Group, pp. 1352–1360, 2016.","apa":"Salzer, E., Çaǧdaş, D., Hons, M., Mace, E., Garncarz, W., Petronczki, O., … Boztug, K. (2016). RASGRP1 deficiency causes immunodeficiency with impaired cytoskeletal dynamics. Nature Immunology. Nature Publishing Group. https://doi.org/10.1038/ni.3575","mla":"Salzer, Elisabeth, et al. “RASGRP1 Deficiency Causes Immunodeficiency with Impaired Cytoskeletal Dynamics.” Nature Immunology, vol. 17, no. 12, Nature Publishing Group, 2016, pp. 1352–60, doi:10.1038/ni.3575.","short":"E. Salzer, D. Çaǧdaş, M. Hons, E. Mace, W. Garncarz, O. Petronczki, R. Platzer, L. Pfajfer, I. Bilic, S. Ban, K. Willmann, M. Mukherjee, V. Supper, H. Hsu, P. Banerjee, P. Sinha, F. Mcclanahan, G. Zlabinger, W. Pickl, J. Gribben, H. Stockinger, K. Bennett, J. Huppa, L. Dupré, Ö. Sanal, U. Jäger, M.K. Sixt, I. Tezcan, J. Orange, K. Boztug, Nature Immunology 17 (2016) 1352–1360.","chicago":"Salzer, Elisabeth, Deniz Çaǧdaş, Miroslav Hons, Emily Mace, Wojciech Garncarz, Oezlem Petronczki, René Platzer, et al. “RASGRP1 Deficiency Causes Immunodeficiency with Impaired Cytoskeletal Dynamics.” Nature Immunology. Nature Publishing Group, 2016. https://doi.org/10.1038/ni.3575."},"article_type":"original","page":"1352 - 1360","date_published":"2016-12-01T00:00:00Z","type":"journal_article","abstract":[{"lang":"eng","text":"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."}],"issue":"12","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"1137","status":"public","title":"RASGRP1 deficiency causes immunodeficiency with impaired cytoskeletal dynamics","intvolume":" 17","oa_version":"Submitted Version","month":"12","external_id":{"pmid":["27776107"]},"oa":1,"main_file_link":[{"url":"https://www.ncbi.nlm.nih.gov/pmc/articles/PMC6400263","open_access":"1"}],"quality_controlled":"1","doi":"10.1038/ni.3575","language":[{"iso":"eng"}],"publist_id":"6221","year":"2016","pmid":1,"publication_status":"published","publisher":"Nature Publishing Group","department":[{"_id":"MiSi"}],"author":[{"last_name":"Salzer","first_name":"Elisabeth","full_name":"Salzer, Elisabeth"},{"full_name":"Çaǧdaş, Deniz","last_name":"Çaǧdaş","first_name":"Deniz"},{"full_name":"Hons, Miroslav","first_name":"Miroslav","last_name":"Hons","id":"4167FE56-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-6625-3348"},{"full_name":"Mace, Emily","first_name":"Emily","last_name":"Mace"},{"full_name":"Garncarz, Wojciech","first_name":"Wojciech","last_name":"Garncarz"},{"last_name":"Petronczki","first_name":"Oezlem","full_name":"Petronczki, Oezlem"},{"last_name":"Platzer","first_name":"René","full_name":"Platzer, René"},{"full_name":"Pfajfer, Laurène","first_name":"Laurène","last_name":"Pfajfer"},{"first_name":"Ivan","last_name":"Bilic","full_name":"Bilic, Ivan"},{"full_name":"Ban, Sol","last_name":"Ban","first_name":"Sol"},{"full_name":"Willmann, Katharina","first_name":"Katharina","last_name":"Willmann"},{"first_name":"Malini","last_name":"Mukherjee","full_name":"Mukherjee, Malini"},{"first_name":"Verena","last_name":"Supper","full_name":"Supper, Verena"},{"full_name":"Hsu, Hsiangting","first_name":"Hsiangting","last_name":"Hsu"},{"full_name":"Banerjee, Pinaki","first_name":"Pinaki","last_name":"Banerjee"},{"full_name":"Sinha, Papiya","first_name":"Papiya","last_name":"Sinha"},{"last_name":"Mcclanahan","first_name":"Fabienne","full_name":"Mcclanahan, Fabienne"},{"full_name":"Zlabinger, Gerhard","first_name":"Gerhard","last_name":"Zlabinger"},{"last_name":"Pickl","first_name":"Winfried","full_name":"Pickl, Winfried"},{"full_name":"Gribben, John","last_name":"Gribben","first_name":"John"},{"last_name":"Stockinger","first_name":"Hannes","full_name":"Stockinger, Hannes"},{"full_name":"Bennett, Keiryn","last_name":"Bennett","first_name":"Keiryn"},{"last_name":"Huppa","first_name":"Johannes","full_name":"Huppa, Johannes"},{"first_name":"Loï̈C","last_name":"Dupré","full_name":"Dupré, Loï̈C"},{"full_name":"Sanal, Özden","first_name":"Özden","last_name":"Sanal"},{"last_name":"Jäger","first_name":"Ulrich","full_name":"Jäger, Ulrich"},{"orcid":"0000-0002-6620-9179","id":"41E9FBEA-F248-11E8-B48F-1D18A9856A87","last_name":"Sixt","first_name":"Michael K","full_name":"Sixt, Michael K"},{"first_name":"Ilhan","last_name":"Tezcan","full_name":"Tezcan, Ilhan"},{"full_name":"Orange, Jordan","first_name":"Jordan","last_name":"Orange"},{"last_name":"Boztug","first_name":"Kaan","full_name":"Boztug, Kaan"}],"date_updated":"2021-01-12T06:48:33Z","date_created":"2018-12-11T11:50:21Z","volume":17},{"scopus_import":1,"day":"05","publication":"Proceedings of the 31st Annual ACM/IEEE Symposium","citation":{"chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Quantitative Automata under Probabilistic Semantics.” In Proceedings of the 31st Annual ACM/IEEE Symposium, 76–85. IEEE, 2016. https://doi.org/10.1145/2933575.2933588.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, Proceedings of the 31st Annual ACM/IEEE Symposium, IEEE, 2016, pp. 76–85.","mla":"Chatterjee, Krishnendu, et al. “Quantitative Automata under Probabilistic Semantics.” Proceedings of the 31st Annual ACM/IEEE Symposium, IEEE, 2016, pp. 76–85, doi:10.1145/2933575.2933588.","apa":"Chatterjee, K., Henzinger, T. A., & Otop, J. (2016). Quantitative automata under probabilistic semantics. In Proceedings of the 31st Annual ACM/IEEE Symposium (pp. 76–85). New York, NY, USA: IEEE. https://doi.org/10.1145/2933575.2933588","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Quantitative automata under probabilistic semantics,” in Proceedings of the 31st Annual ACM/IEEE Symposium, New York, NY, USA, 2016, pp. 76–85.","ista":"Chatterjee K, Henzinger TA, Otop J. 2016. Quantitative automata under probabilistic semantics. Proceedings of the 31st Annual ACM/IEEE Symposium. LICS: Logic in Computer Science, 76–85.","ama":"Chatterjee K, Henzinger TA, Otop J. Quantitative automata under probabilistic semantics. In: Proceedings of the 31st Annual ACM/IEEE Symposium. IEEE; 2016:76-85. doi:10.1145/2933575.2933588"},"page":"76 - 85","date_published":"2016-07-05T00:00:00Z","type":"conference","abstract":[{"lang":"eng","text":"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."}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"1138","status":"public","title":"Quantitative automata under probabilistic semantics","oa_version":"Preprint","month":"07","external_id":{"arxiv":["1604.06764"]},"oa":1,"main_file_link":[{"url":"https://arxiv.org/abs/1604.06764","open_access":"1"}],"quality_controlled":"1","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003"}],"conference":{"start_date":"2016-07-05","location":"New York, NY, USA","end_date":"2016-07-08","name":"LICS: Logic in Computer Science"},"doi":"10.1145/2933575.2933588","language":[{"iso":"eng"}],"ec_funded":1,"publist_id":"6220","acknowledgement":"This research was funded in part by the European Research Council (ERC) under grant agreement 267989 (QUAREM), by the Austrian Science Fund (FWF) projects S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award), FWF Grant No P23499- N23, FWF NFN Grant No S114","year":"2016","publication_status":"published","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publisher":"IEEE","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger"},{"full_name":"Otop, Jan","first_name":"Jan","last_name":"Otop","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87"}],"date_updated":"2021-01-12T06:48:34Z","date_created":"2018-12-11T11:50:21Z"},{"oa":1,"external_id":{"arxiv":["1602.02670"]},"main_file_link":[{"url":"https://arxiv.org/abs/1602.02670","open_access":"1"}],"quality_controlled":"1","project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003"}],"conference":{"start_date":"2016-07-05","location":"New York, NY, USA","end_date":"2016-07-08","name":"LICS: Logic in Computer Science"},"doi":"10.1145/2933575.2935304","language":[{"iso":"eng"}],"month":"07","acknowledgement":"K. C., M. H., and W. D. are partially supported by the Vienna\r\nScience and Technology Fund (WWTF) through project ICT15-003.\r\nK. C. is partially supported by the Austrian Science Fund (FWF)\r\nNFN Grant No S11407-N23 (RiSE/SHiNE) and an ERC Start grant\r\n(279307: Graph Games). For W. D., M. H., and V. L. the research\r\nleading to these results has received funding from the European\r\nResearch Council under the European Union’s Seventh Framework\r\nProgramme (FP/2007-2013) / ERC Grant Agreement no. 340506.","year":"2016","publication_status":"published","department":[{"_id":"KrCh"}],"publisher":"IEEE","author":[{"first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"full_name":"Dvoák, Wolfgang","last_name":"Dvoák","first_name":"Wolfgang"},{"full_name":"Henzinger, Monika H","first_name":"Monika H","last_name":"Henzinger","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","orcid":"0000-0002-5008-6530"},{"full_name":"Loitzenbauer, Veronika","first_name":"Veronika","last_name":"Loitzenbauer"}],"date_updated":"2022-09-09T11:46:17Z","date_created":"2018-12-11T11:50:22Z","publist_id":"6219","publication":"Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science","citation":{"short":"K. Chatterjee, W. Dvoák, M.H. Henzinger, V. Loitzenbauer, in:, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, IEEE, 2016, pp. 197–206.","mla":"Chatterjee, Krishnendu, et al. “Model and Objective Separation with Conditional Lower Bounds: Disjunction Is Harder than Conjunction.” Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, IEEE, 2016, pp. 197–206, doi:10.1145/2933575.2935304.","chicago":"Chatterjee, Krishnendu, Wolfgang Dvoák, Monika H Henzinger, and Veronika Loitzenbauer. “Model and Objective Separation with Conditional Lower Bounds: Disjunction Is Harder than Conjunction.” In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, 197–206. IEEE, 2016. https://doi.org/10.1145/2933575.2935304.","ama":"Chatterjee K, Dvoák W, Henzinger MH, Loitzenbauer V. Model and objective separation with conditional lower bounds: disjunction is harder than conjunction. In: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science. IEEE; 2016:197-206. doi:10.1145/2933575.2935304","apa":"Chatterjee, K., Dvoák, W., Henzinger, M. H., & Loitzenbauer, V. (2016). Model and objective separation with conditional lower bounds: disjunction is harder than conjunction. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (pp. 197–206). New York, NY, USA: IEEE. https://doi.org/10.1145/2933575.2935304","ieee":"K. Chatterjee, W. Dvoák, M. H. Henzinger, and V. Loitzenbauer, “Model and objective separation with conditional lower bounds: disjunction is harder than conjunction,” in Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, New York, NY, USA, 2016, pp. 197–206.","ista":"Chatterjee K, Dvoák W, Henzinger MH, Loitzenbauer V. 2016. Model and objective separation with conditional lower bounds: disjunction is harder than conjunction. Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science. LICS: Logic in Computer Science, Proceedings Symposium on Logic in Computer Science, , 197–206."},"page":"197 - 206","date_published":"2016-07-05T00:00:00Z","scopus_import":"1","day":"05","article_processing_charge":"No","_id":"1140","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","title":"Model and objective separation with conditional lower bounds: disjunction is harder than conjunction","oa_version":"Preprint","type":"conference","alternative_title":["Proceedings Symposium on Logic in Computer Science"],"abstract":[{"lang":"eng","text":"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."}]}]