[{"ec_funded":1,"citation":{"short":"V. Forejt, J. Krčál, J. Kretinsky, in:, Springer, 2015, pp. 162–177.","ama":"Forejt V, Krčál J, Kretinsky J. Controller synthesis for MDPs and frequency LTL\\GU. In: Vol 9450. Springer; 2015:162-177. doi:<a href=\"https://doi.org/10.1007/978-3-662-48899-7_12\">10.1007/978-3-662-48899-7_12</a>","apa":"Forejt, V., Krčál, J., &#38; Kretinsky, J. (2015). Controller synthesis for MDPs and frequency LTL\\GU (Vol. 9450, pp. 162–177). Presented at the LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, Suva, Fiji: Springer. <a href=\"https://doi.org/10.1007/978-3-662-48899-7_12\">https://doi.org/10.1007/978-3-662-48899-7_12</a>","chicago":"Forejt, Vojtěch, Jan Krčál, and Jan Kretinsky. “Controller Synthesis for MDPs and Frequency LTL\\GU,” 9450:162–77. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-662-48899-7_12\">https://doi.org/10.1007/978-3-662-48899-7_12</a>.","ieee":"V. Forejt, J. Krčál, and J. Kretinsky, “Controller synthesis for MDPs and frequency LTL\\GU,” presented at the LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, Suva, Fiji, 2015, vol. 9450, pp. 162–177.","ista":"Forejt V, Krčál J, Kretinsky J. 2015. Controller synthesis for MDPs and frequency LTL\\GU. LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, LNCS, vol. 9450, 162–177.","mla":"Forejt, Vojtěch, et al. <i>Controller Synthesis for MDPs and Frequency LTL\\GU</i>. Vol. 9450, Springer, 2015, pp. 162–77, doi:<a href=\"https://doi.org/10.1007/978-3-662-48899-7_12\">10.1007/978-3-662-48899-7_12</a>."},"conference":{"end_date":"2015-11-28","start_date":"2015-11-24","name":"LPAR: Logic for Programming, Artificial Intelligence, and Reasoning","location":"Suva, Fiji"},"title":"Controller synthesis for MDPs and frequency LTL\\GU","day":"22","alternative_title":["LNCS"],"type":"conference","author":[{"last_name":"Forejt","full_name":"Forejt, Vojtěch","first_name":"Vojtěch"},{"last_name":"Krčál","full_name":"Krčál, Jan","first_name":"Jan"},{"orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","last_name":"Kretinsky","full_name":"Kretinsky, Jan","first_name":"Jan"}],"acknowledgement":"This work is partly supported by the German Research Council (DFG) as part of the Transregional Collaborative Research Center AVACS (SFB/TR 14), by the Czech Science Foundation under grant agreement P202/12/G061, by the EU 7th Framework Programme under grant agreement no. 295261 (MEALS) and 318490 (SENSATION), by the CDZ project 1023 (CAP), by the CAS/SAFEA International Partnership Program for Creative Research Teams, by the EPSRC grant EP/M023656/1, by the People Programme (Marie Curie Actions) of the European Union’s Seventh Framework Programme (FP7/2007–2013) REA Grant No 291734, by the Austrian Science Fund (FWF) S11407-N23 (RiSE/SHiNE), and by the ERC Start Grant (279307: Graph Games).\r\n","project":[{"call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734","name":"International IST Postdoc Fellowship Programme"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"}],"language":[{"iso":"eng"}],"doi":"10.1007/978-3-662-48899-7_12","page":"162 - 177","month":"11","date_created":"2018-12-11T11:52:55Z","publisher":"Springer","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"quality_controlled":"1","intvolume":"      9450","status":"public","publist_id":"5577","year":"2015","oa_version":"None","date_updated":"2021-01-12T06:51:50Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","scopus_import":1,"_id":"1594","date_published":"2015-11-22T00:00:00Z","abstract":[{"lang":"eng","text":"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."}],"publication_status":"published","volume":9450},{"citation":{"apa":"Fulek, R., Pelsmajer, M., &#38; Schaefer, M. (2015). Hanani-Tutte for radial planarity (Vol. 9411, pp. 99–110). Presented at the GD: Graph Drawing and Network Visualization, Los Angeles, CA, USA: Springer. <a href=\"https://doi.org/10.1007/978-3-319-27261-0_9\">https://doi.org/10.1007/978-3-319-27261-0_9</a>","ama":"Fulek R, Pelsmajer M, Schaefer M. Hanani-Tutte for radial planarity. In: Vol 9411. Springer; 2015:99-110. doi:<a href=\"https://doi.org/10.1007/978-3-319-27261-0_9\">10.1007/978-3-319-27261-0_9</a>","short":"R. Fulek, M. Pelsmajer, M. Schaefer, in:, Springer, 2015, pp. 99–110.","mla":"Fulek, Radoslav, et al. <i>Hanani-Tutte for Radial Planarity</i>. Vol. 9411, Springer, 2015, pp. 99–110, doi:<a href=\"https://doi.org/10.1007/978-3-319-27261-0_9\">10.1007/978-3-319-27261-0_9</a>.","ista":"Fulek R, Pelsmajer M, Schaefer M. 2015. Hanani-Tutte for radial planarity. GD: Graph Drawing and Network Visualization, LNCS, vol. 9411, 99–110.","ieee":"R. Fulek, M. Pelsmajer, and M. Schaefer, “Hanani-Tutte for radial planarity,” presented at the GD: Graph Drawing and Network Visualization, Los Angeles, CA, USA, 2015, vol. 9411, pp. 99–110.","chicago":"Fulek, Radoslav, Michael Pelsmajer, and Marcus Schaefer. “Hanani-Tutte for Radial Planarity,” 9411:99–110. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-319-27261-0_9\">https://doi.org/10.1007/978-3-319-27261-0_9</a>."},"ec_funded":1,"title":"Hanani-Tutte for radial planarity","conference":{"location":"Los Angeles, CA, USA","name":"GD: Graph Drawing and Network Visualization","end_date":"2015-09-26","start_date":"2015-09-24"},"day":"27","type":"conference","author":[{"last_name":"Fulek","full_name":"Fulek, Radoslav","first_name":"Radoslav","orcid":"0000-0001-8485-1774","id":"39F3FFE4-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Pelsmajer","first_name":"Michael","full_name":"Pelsmajer, Michael"},{"last_name":"Schaefer","full_name":"Schaefer, Marcus","first_name":"Marcus"}],"alternative_title":["LNCS"],"project":[{"_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"291734","name":"International IST Postdoc Fellowship Programme"}],"related_material":{"record":[{"relation":"later_version","id":"1113","status":"public"},{"relation":"later_version","id":"1164","status":"public"}]},"acknowledgement":"The research leading to these results has received funding from the People Programme (Marie Curie Actions) of the European Union’s Seventh Framework Programme (FP7/2007-2013) under REA grant agreement no [291734].","language":[{"iso":"eng"}],"ddc":["510"],"doi":"10.1007/978-3-319-27261-0_9","page":"99 - 110","month":"11","date_created":"2018-12-11T11:52:55Z","publisher":"Springer","quality_controlled":"1","department":[{"_id":"UlWa"}],"status":"public","intvolume":"      9411","publist_id":"5576","year":"2015","has_accepted_license":"1","oa_version":"Submitted Version","scopus_import":1,"date_updated":"2023-02-21T16:23:36Z","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","file":[{"file_id":"4697","relation":"main_file","content_type":"application/pdf","date_created":"2018-12-12T10:08:36Z","creator":"system","file_size":330135,"file_name":"IST-2016-594-v1+1_HTCylinder_GD_Revision.pdf","checksum":"685f91bd077a951ba067d42cce75409e","access_level":"open_access","date_updated":"2020-07-14T12:45:03Z"}],"abstract":[{"text":"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.","lang":"eng"}],"_id":"1595","date_published":"2015-11-27T00:00:00Z","publication_status":"published","oa":1,"file_date_updated":"2020-07-14T12:45:03Z","pubrep_id":"594","volume":9411},{"publication":"Graph Drawing and Network Visualization","department":[{"_id":"UlWa"}],"quality_controlled":"1","status":"public","intvolume":"      9411","publisher":"Springer Nature","month":"11","date_created":"2018-12-11T11:52:56Z","page":"373 - 379","language":[{"iso":"eng"}],"doi":"10.1007/978-3-319-27261-0_31","ddc":["510"],"project":[{"name":"International IST Postdoc Fellowship Programme","grant_number":"291734","call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425"}],"day":"27","type":"book_chapter","author":[{"last_name":"Fulek","full_name":"Fulek, Radoslav","first_name":"Radoslav","id":"39F3FFE4-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-8485-1774"},{"first_name":"Radoš","full_name":"Radoičić, Radoš","last_name":"Radoičić"}],"alternative_title":["LNCS"],"citation":{"mla":"Fulek, Radoslav, and Radoš Radoičić. “Vertical Visibility among Parallel Polygons in Three Dimensions.” <i>Graph Drawing and Network Visualization</i>, vol. 9411, Springer Nature, 2015, pp. 373–79, doi:<a href=\"https://doi.org/10.1007/978-3-319-27261-0_31\">10.1007/978-3-319-27261-0_31</a>.","ista":"Fulek R, Radoičić R. 2015.Vertical visibility among parallel polygons in three dimensions. In: Graph Drawing and Network Visualization. LNCS, vol. 9411, 373–379.","ieee":"R. Fulek and R. Radoičić, “Vertical visibility among parallel polygons in three dimensions,” in <i>Graph Drawing and Network Visualization</i>, vol. 9411, Springer Nature, 2015, pp. 373–379.","chicago":"Fulek, Radoslav, and Radoš Radoičić. “Vertical Visibility among Parallel Polygons in Three Dimensions.” In <i>Graph Drawing and Network Visualization</i>, 9411:373–79. Springer Nature, 2015. <a href=\"https://doi.org/10.1007/978-3-319-27261-0_31\">https://doi.org/10.1007/978-3-319-27261-0_31</a>.","apa":"Fulek, R., &#38; Radoičić, R. (2015). Vertical visibility among parallel polygons in three dimensions. In <i>Graph Drawing and Network Visualization</i> (Vol. 9411, pp. 373–379). Los Angeles, CA, United States: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-319-27261-0_31\">https://doi.org/10.1007/978-3-319-27261-0_31</a>","ama":"Fulek R, Radoičić R. Vertical visibility among parallel polygons in three dimensions. In: <i>Graph Drawing and Network Visualization</i>. Vol 9411. Springer Nature; 2015:373-379. doi:<a href=\"https://doi.org/10.1007/978-3-319-27261-0_31\">10.1007/978-3-319-27261-0_31</a>","short":"R. Fulek, R. Radoičić, in:, Graph Drawing and Network Visualization, Springer Nature, 2015, pp. 373–379."},"ec_funded":1,"title":"Vertical visibility among parallel polygons in three dimensions","conference":{"location":"Los Angeles, CA, United States","end_date":"2015-09-26","start_date":"2015-09-24","name":"GD: Graph Drawing and Network Visualization"},"file_date_updated":"2020-07-14T12:45:04Z","pubrep_id":"595","volume":9411,"publication_status":"published","oa":1,"file":[{"date_created":"2018-12-12T10:17:06Z","relation":"main_file","file_id":"5258","content_type":"application/pdf","access_level":"open_access","date_updated":"2020-07-14T12:45:04Z","checksum":"eec04f86c5921d04f025d5791db9b965","creator":"system","file_size":312992,"file_name":"IST-2016-595-v1+1_VerticalVisibilityGDRevision.pdf"}],"_id":"1596","date_published":"2015-11-27T00:00:00Z","abstract":[{"text":"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 &lt; j the intersection Ci and (Ci ∩ Cj)\\⋃i&lt;l&lt;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.","lang":"eng"}],"article_processing_charge":"No","scopus_import":"1","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","date_updated":"2022-01-28T09:20:50Z","publication_identifier":{"isbn":["978-3-319-27260-3"]},"publist_id":"5575","has_accepted_license":"1","oa_version":"Submitted Version","year":"2015"},{"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2023-02-23T10:55:03Z","scopus_import":1,"external_id":{"arxiv":["1202.4175"]},"publist_id":"5571","oa_version":"Preprint","year":"2015","publication_status":"published","main_file_link":[{"url":"http://arxiv.org/abs/1202.4175","open_access":"1"}],"oa":1,"volume":573,"arxiv":1,"issue":"3","article_processing_charge":"No","date_published":"2015-03-30T00:00:00Z","_id":"1598","abstract":[{"text":"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.","lang":"eng"}],"acknowledgement":"The research was supported by FWF Grant No. P 23499-N23, FWF NFN Grant No. S11407-N23 (RiSE), ERC Start Grant (279307: Graph Games), and the Microsoft Faculty Fellows Award. Nisarg Shah is also supported by NSF Grant CCF-1215883.\r\n","project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","grant_number":"S11407"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"related_material":{"record":[{"status":"public","relation":"earlier_version","id":"2715"}]},"language":[{"iso":"eng"}],"doi":"10.1016/j.tcs.2015.01.050","ec_funded":1,"citation":{"ama":"Chatterjee K, Joglekar M, Shah N. Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives. <i>Theoretical Computer Science</i>. 2015;573(3):71-89. doi:<a href=\"https://doi.org/10.1016/j.tcs.2015.01.050\">10.1016/j.tcs.2015.01.050</a>","apa":"Chatterjee, K., Joglekar, M., &#38; Shah, N. (2015). Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.tcs.2015.01.050\">https://doi.org/10.1016/j.tcs.2015.01.050</a>","short":"K. Chatterjee, M. Joglekar, N. Shah, Theoretical Computer Science 573 (2015) 71–89.","mla":"Chatterjee, Krishnendu, et al. “Average Case Analysis of the Classical Algorithm for Markov Decision Processes with Büchi Objectives.” <i>Theoretical Computer Science</i>, vol. 573, no. 3, Elsevier, 2015, pp. 71–89, doi:<a href=\"https://doi.org/10.1016/j.tcs.2015.01.050\">10.1016/j.tcs.2015.01.050</a>.","chicago":"Chatterjee, Krishnendu, Manas Joglekar, and Nisarg Shah. “Average Case Analysis of the Classical Algorithm for Markov Decision Processes with Büchi Objectives.” <i>Theoretical Computer Science</i>. Elsevier, 2015. <a href=\"https://doi.org/10.1016/j.tcs.2015.01.050\">https://doi.org/10.1016/j.tcs.2015.01.050</a>.","ieee":"K. Chatterjee, M. Joglekar, and N. Shah, “Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives,” <i>Theoretical Computer Science</i>, vol. 573, no. 3. Elsevier, pp. 71–89, 2015.","ista":"Chatterjee K, Joglekar M, Shah N. 2015. Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives. Theoretical Computer Science. 573(3), 71–89."},"title":"Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives","day":"30","type":"journal_article","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"last_name":"Joglekar","full_name":"Joglekar, Manas","first_name":"Manas"},{"last_name":"Shah","full_name":"Shah, Nisarg","first_name":"Nisarg"}],"publisher":"Elsevier","quality_controlled":"1","department":[{"_id":"KrCh"}],"publication":"Theoretical Computer Science","status":"public","intvolume":"       573","page":"71 - 89","month":"03","date_created":"2018-12-11T11:52:56Z"},{"page":"479 - 486","date_created":"2018-12-11T11:52:57Z","month":"07","publisher":"Springer","status":"public","intvolume":"      9206","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"quality_controlled":"1","conference":{"name":"CAV: Computer Aided Verification","end_date":"2015-07-24","start_date":"2015-07-18","location":"San Francisco, CA, United States"},"title":"The Hanoi omega-automata format","ec_funded":1,"citation":{"short":"T. Babiak, F. Blahoudek, A. Duret Lutz, J. Klein, J. Kretinsky, D. Mueller, D. Parker, J. Strejček, in:, Springer, 2015, pp. 479–486.","apa":"Babiak, T., Blahoudek, F., Duret Lutz, A., Klein, J., Kretinsky, J., Mueller, D., … Strejček, J. (2015). The Hanoi omega-automata format (Vol. 9206, pp. 479–486). Presented at the CAV: Computer Aided Verification, San Francisco, CA, United States: Springer. <a href=\"https://doi.org/10.1007/978-3-319-21690-4_31\">https://doi.org/10.1007/978-3-319-21690-4_31</a>","ama":"Babiak T, Blahoudek F, Duret Lutz A, et al. The Hanoi omega-automata format. In: Vol 9206. Springer; 2015:479-486. doi:<a href=\"https://doi.org/10.1007/978-3-319-21690-4_31\">10.1007/978-3-319-21690-4_31</a>","ieee":"T. Babiak <i>et al.</i>, “The Hanoi omega-automata format,” presented at the CAV: Computer Aided Verification, San Francisco, CA, United States, 2015, vol. 9206, pp. 479–486.","ista":"Babiak T, Blahoudek F, Duret Lutz A, Klein J, Kretinsky J, Mueller D, Parker D, Strejček J. 2015. The Hanoi omega-automata format. CAV: Computer Aided Verification, LNCS, vol. 9206, 479–486.","chicago":"Babiak, Tomáš, František Blahoudek, Alexandre Duret Lutz, Joachim Klein, Jan Kretinsky, Daniel Mueller, David Parker, and Jan Strejček. “The Hanoi Omega-Automata Format,” 9206:479–86. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-319-21690-4_31\">https://doi.org/10.1007/978-3-319-21690-4_31</a>.","mla":"Babiak, Tomáš, et al. <i>The Hanoi Omega-Automata Format</i>. Vol. 9206, Springer, 2015, pp. 479–86, doi:<a href=\"https://doi.org/10.1007/978-3-319-21690-4_31\">10.1007/978-3-319-21690-4_31</a>."},"alternative_title":["LNCS"],"author":[{"last_name":"Babiak","full_name":"Babiak, Tomáš","first_name":"Tomáš"},{"full_name":"Blahoudek, František","first_name":"František","last_name":"Blahoudek"},{"last_name":"Duret Lutz","full_name":"Duret Lutz, Alexandre","first_name":"Alexandre"},{"last_name":"Klein","full_name":"Klein, Joachim","first_name":"Joachim"},{"orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","full_name":"Kretinsky, Jan","first_name":"Jan","last_name":"Kretinsky"},{"last_name":"Mueller","full_name":"Mueller, Daniel","first_name":"Daniel"},{"first_name":"David","full_name":"Parker, David","last_name":"Parker"},{"full_name":"Strejček, Jan","first_name":"Jan","last_name":"Strejček"}],"type":"conference","day":"16","project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211"},{"_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"International IST Postdoc Fellowship Programme","grant_number":"291734"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"}],"ddc":["000"],"doi":"10.1007/978-3-319-21690-4_31","language":[{"iso":"eng"}],"article_processing_charge":"No","date_published":"2015-07-16T00:00:00Z","_id":"1601","abstract":[{"text":"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.","lang":"eng"}],"file":[{"file_size":1651779,"creator":"dernst","file_name":"2015_CAV_Babiak.pdf","access_level":"open_access","date_updated":"2020-07-14T12:45:04Z","checksum":"5885236fa88a439baba9ac6f3e801e93","relation":"main_file","file_id":"7850","content_type":"application/pdf","date_created":"2020-05-15T08:38:12Z"}],"oa":1,"publication_status":"published","volume":9206,"file_date_updated":"2020-07-14T12:45:04Z","has_accepted_license":"1","oa_version":"Submitted Version","year":"2015","publist_id":"5566","date_updated":"2021-01-12T06:51:54Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","scopus_import":1},{"ec_funded":1,"citation":{"chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, Andreas Pavlogiannis, and Prateesh Goyal. “Faster Algorithms for Algebraic Path Properties in Recursive State Machines with Constant Treewidth.” <i>ACM SIGPLAN Notices</i>. ACM, 2015. <a href=\"https://doi.org/10.1145/2676726.2676979\">https://doi.org/10.1145/2676726.2676979</a>.","ieee":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, and P. Goyal, “Faster algorithms for algebraic path properties in recursive state machines with constant treewidth,” <i>ACM SIGPLAN Notices</i>, vol. 50, no. 1. ACM, pp. 97–109, 2015.","ista":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A, Goyal P. 2015. Faster algorithms for algebraic path properties in recursive state machines with constant treewidth. ACM SIGPLAN Notices. 50(1), 97–109.","mla":"Chatterjee, Krishnendu, et al. “Faster Algorithms for Algebraic Path Properties in Recursive State Machines with Constant Treewidth.” <i>ACM SIGPLAN Notices</i>, vol. 50, no. 1, ACM, 2015, pp. 97–109, doi:<a href=\"https://doi.org/10.1145/2676726.2676979\">10.1145/2676726.2676979</a>.","short":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, P. Goyal, ACM SIGPLAN Notices 50 (2015) 97–109.","ama":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A, Goyal P. Faster algorithms for algebraic path properties in recursive state machines with constant treewidth. <i>ACM SIGPLAN Notices</i>. 2015;50(1):97-109. doi:<a href=\"https://doi.org/10.1145/2676726.2676979\">10.1145/2676726.2676979</a>","apa":"Chatterjee, K., Ibsen-Jensen, R., Pavlogiannis, A., &#38; Goyal, P. (2015). Faster algorithms for algebraic path properties in recursive state machines with constant treewidth. <i>ACM SIGPLAN Notices</i>. Mumbai, India: ACM. <a href=\"https://doi.org/10.1145/2676726.2676979\">https://doi.org/10.1145/2676726.2676979</a>"},"conference":{"end_date":"2015-01-17","start_date":"2015-01-15","name":"SIGPLAN: Symposium on Principles of Programming Languages","location":"Mumbai, India"},"title":"Faster algorithms for algebraic path properties in recursive state machines with constant treewidth","day":"01","type":"journal_article","author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389","last_name":"Ibsen-Jensen","first_name":"Rasmus","full_name":"Ibsen-Jensen, Rasmus"},{"last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas","first_name":"Andreas","orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Prateesh","full_name":"Goyal, Prateesh","last_name":"Goyal"}],"acknowledgement":"We thank anonymous reviewers for helpful comments to improve the presentation of the paper.","project":[{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"related_material":{"record":[{"relation":"dissertation_contains","id":"821","status":"public"}]},"language":[{"iso":"eng"}],"doi":"10.1145/2676726.2676979","page":"97 - 109","month":"01","date_created":"2018-12-11T11:52:58Z","publisher":"ACM","quality_controlled":"1","department":[{"_id":"KrCh"}],"publication":"ACM SIGPLAN Notices","status":"public","intvolume":"        50","publist_id":"5565","oa_version":"Preprint","year":"2015","date_updated":"2023-09-07T12:01:58Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","scopus_import":1,"external_id":{"arxiv":["1410.7724"]},"arxiv":1,"issue":"1","date_published":"2015-01-01T00:00:00Z","_id":"1602","abstract":[{"text":"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.","lang":"eng"}],"publication_status":"published","oa":1,"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1410.7724"}],"volume":50},{"doi":"10.1007/978-3-319-21690-4_10","language":[{"iso":"eng"}],"related_material":{"record":[{"status":"public","id":"5549","relation":"research_paper"}]},"project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"name":"Quantitative Reactive Modeling","grant_number":"267989","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"grant_number":"291734","name":"International IST Postdoc Fellowship Programme","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"acknowledgement":"This research was funded in part by Austrian Science Fund (FWF) Grant No P 23499-N23, FWF NFN Grant No S11407-N23 (RiSE) and Z211-N23 (Wittgenstein Award), European Research Council (ERC) Grant No 279307 (Graph Games), ERC Grant No 267989 (QUAREM), the Czech Science Foundation Grant No P202/12/G061, and People Programme (Marie Curie Actions) of the European Union’s Seventh Framework Programme (FP7/2007–2013) REA Grant No 291734.","author":[{"last_name":"Brázdil","first_name":"Tomáš","full_name":"Brázdil, Tomáš"},{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"full_name":"Chmelik, Martin","first_name":"Martin","last_name":"Chmelik","id":"3624234E-F248-11E8-B48F-1D18A9856A87"},{"id":"42BABFB4-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas","full_name":"Fellner, Andreas","last_name":"Fellner"},{"orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","full_name":"Kretinsky, Jan","last_name":"Kretinsky"}],"type":"conference","alternative_title":["LNCS"],"day":"16","title":"Counterexample explanation by learning small strategies in Markov decision processes","conference":{"location":"San Francisco, CA, United States","end_date":"2015-07-24","start_date":"2015-07-18","name":"CAV: Computer Aided Verification"},"citation":{"apa":"Brázdil, T., Chatterjee, K., Chmelik, M., Fellner, A., &#38; Kretinsky, J. (2015). Counterexample explanation by learning small strategies in Markov decision processes (Vol. 9206, pp. 158–177). Presented at the CAV: Computer Aided Verification, San Francisco, CA, United States: Springer. <a href=\"https://doi.org/10.1007/978-3-319-21690-4_10\">https://doi.org/10.1007/978-3-319-21690-4_10</a>","ama":"Brázdil T, Chatterjee K, Chmelik M, Fellner A, Kretinsky J. Counterexample explanation by learning small strategies in Markov decision processes. In: Vol 9206. Springer; 2015:158-177. doi:<a href=\"https://doi.org/10.1007/978-3-319-21690-4_10\">10.1007/978-3-319-21690-4_10</a>","short":"T. Brázdil, K. Chatterjee, M. Chmelik, A. Fellner, J. Kretinsky, in:, Springer, 2015, pp. 158–177.","mla":"Brázdil, Tomáš, et al. <i>Counterexample Explanation by Learning Small Strategies in Markov Decision Processes</i>. Vol. 9206, Springer, 2015, pp. 158–77, doi:<a href=\"https://doi.org/10.1007/978-3-319-21690-4_10\">10.1007/978-3-319-21690-4_10</a>.","ista":"Brázdil T, Chatterjee K, Chmelik M, Fellner A, Kretinsky J. 2015. Counterexample explanation by learning small strategies in Markov decision processes. CAV: Computer Aided Verification, LNCS, vol. 9206, 158–177.","ieee":"T. Brázdil, K. Chatterjee, M. Chmelik, A. Fellner, and J. Kretinsky, “Counterexample explanation by learning small strategies in Markov decision processes,” presented at the CAV: Computer Aided Verification, San Francisco, CA, United States, 2015, vol. 9206, pp. 158–177.","chicago":"Brázdil, Tomáš, Krishnendu Chatterjee, Martin Chmelik, Andreas Fellner, and Jan Kretinsky. “Counterexample Explanation by Learning Small Strategies in Markov Decision Processes,” 9206:158–77. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-319-21690-4_10\">https://doi.org/10.1007/978-3-319-21690-4_10</a>."},"ec_funded":1,"intvolume":"      9206","status":"public","quality_controlled":"1","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publisher":"Springer","date_created":"2018-12-11T11:52:58Z","month":"07","page":"158 - 177","publication_identifier":{"eisbn":["978-3-319-21690-4"]},"scopus_import":1,"date_updated":"2024-02-21T13:52:07Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"Preprint","year":"2015","publist_id":"5564","volume":9206,"main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1502.02834"}],"oa":1,"publication_status":"published","date_published":"2015-07-16T00:00:00Z","_id":"1603","abstract":[{"lang":"eng","text":"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.\r\nThe 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."}]},{"related_material":{"record":[{"id":"5445","relation":"earlier_version","status":"public"},{"relation":"dissertation_contains","id":"821","status":"public"}]},"project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"language":[{"iso":"eng"}],"doi":"10.1145/2676726.2676968","citation":{"chicago":"Chatterjee, Krishnendu, Andreas Pavlogiannis, and Yaron Velner. “Quantitative Interprocedural Analysis.” <i>Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT </i>. ACM, 2015. <a href=\"https://doi.org/10.1145/2676726.2676968\">https://doi.org/10.1145/2676726.2676968</a>.","ieee":"K. Chatterjee, A. Pavlogiannis, and Y. Velner, “Quantitative interprocedural analysis,” <i>Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT </i>, vol. 50, no. 1. ACM, pp. 539–551, 2015.","ista":"Chatterjee K, Pavlogiannis A, Velner Y. 2015. Quantitative interprocedural analysis. Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT . 50(1), 539–551.","mla":"Chatterjee, Krishnendu, et al. “Quantitative Interprocedural Analysis.” <i>Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT </i>, vol. 50, no. 1, ACM, 2015, pp. 539–51, doi:<a href=\"https://doi.org/10.1145/2676726.2676968\">10.1145/2676726.2676968</a>.","short":"K. Chatterjee, A. Pavlogiannis, Y. Velner, Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT  50 (2015) 539–551.","ama":"Chatterjee K, Pavlogiannis A, Velner Y. Quantitative interprocedural analysis. <i>Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT </i>. 2015;50(1):539-551. doi:<a href=\"https://doi.org/10.1145/2676726.2676968\">10.1145/2676726.2676968</a>","apa":"Chatterjee, K., Pavlogiannis, A., &#38; Velner, Y. (2015). Quantitative interprocedural analysis. <i>Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT </i>. Mumbai, India: ACM. <a href=\"https://doi.org/10.1145/2676726.2676968\">https://doi.org/10.1145/2676726.2676968</a>"},"ec_funded":1,"title":"Quantitative interprocedural analysis","conference":{"location":"Mumbai, India","start_date":"2015-01-15","end_date":"2015-01-17","name":"SIGPLAN: Symposium on Principles of Programming Languages"},"day":"01","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee"},{"last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas","first_name":"Andreas","orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Velner","first_name":"Yaron","full_name":"Velner, Yaron"}],"type":"journal_article","publisher":"ACM","publication":"Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT ","department":[{"_id":"KrCh"}],"quality_controlled":"1","intvolume":"        50","status":"public","page":"539 - 551","month":"01","date_created":"2018-12-11T11:52:59Z","scopus_import":1,"date_updated":"2023-09-07T12:01:59Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_identifier":{"isbn":["978-1-4503-3300-9"]},"publist_id":"5563","oa_version":"None","year":"2015","publication_status":"published","pubrep_id":"523","volume":50,"issue":"1","_id":"1604","date_published":"2015-01-01T00:00:00Z","abstract":[{"lang":"eng","text":"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."}]},{"page":"19 - 35","date_created":"2018-12-11T11:52:59Z","month":"11","publisher":"Springer","status":"public","intvolume":"      9434","department":[{"_id":"ToHe"}],"quality_controlled":"1","title":"Abstraction-based parameter synthesis for multiaffine systems","conference":{"name":"HVC: Haifa Verification Conference","end_date":"2015-11-19","start_date":"2015-11-17","location":"Haifa, Israel"},"citation":{"chicago":"Bogomolov, Sergiy, Christian Schilling, Ezio Bartocci, Grégory Batt, Hui Kong, and Radu Grosu. “Abstraction-Based Parameter Synthesis for Multiaffine Systems,” 9434:19–35. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-319-26287-1_2\">https://doi.org/10.1007/978-3-319-26287-1_2</a>.","ieee":"S. Bogomolov, C. Schilling, E. Bartocci, G. Batt, H. Kong, and R. Grosu, “Abstraction-based parameter synthesis for multiaffine systems,” presented at the HVC: Haifa Verification Conference, Haifa, Israel, 2015, vol. 9434, pp. 19–35.","ista":"Bogomolov S, Schilling C, Bartocci E, Batt G, Kong H, Grosu R. 2015. Abstraction-based parameter synthesis for multiaffine systems. HVC: Haifa Verification Conference, LNCS, vol. 9434, 19–35.","mla":"Bogomolov, Sergiy, et al. <i>Abstraction-Based Parameter Synthesis for Multiaffine Systems</i>. Vol. 9434, Springer, 2015, pp. 19–35, doi:<a href=\"https://doi.org/10.1007/978-3-319-26287-1_2\">10.1007/978-3-319-26287-1_2</a>.","short":"S. Bogomolov, C. Schilling, E. Bartocci, G. Batt, H. Kong, R. Grosu, in:, Springer, 2015, pp. 19–35.","ama":"Bogomolov S, Schilling C, Bartocci E, Batt G, Kong H, Grosu R. Abstraction-based parameter synthesis for multiaffine systems. In: Vol 9434. Springer; 2015:19-35. doi:<a href=\"https://doi.org/10.1007/978-3-319-26287-1_2\">10.1007/978-3-319-26287-1_2</a>","apa":"Bogomolov, S., Schilling, C., Bartocci, E., Batt, G., Kong, H., &#38; Grosu, R. (2015). Abstraction-based parameter synthesis for multiaffine systems (Vol. 9434, pp. 19–35). Presented at the HVC: Haifa Verification Conference, Haifa, Israel: Springer. <a href=\"https://doi.org/10.1007/978-3-319-26287-1_2\">https://doi.org/10.1007/978-3-319-26287-1_2</a>"},"ec_funded":1,"type":"conference","author":[{"last_name":"Bogomolov","full_name":"Bogomolov, Sergiy","first_name":"Sergiy","id":"369D9A44-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-0686-0365"},{"orcid":"0000-0003-3658-1065","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","full_name":"Schilling, Christian","first_name":"Christian","last_name":"Schilling"},{"first_name":"Ezio","full_name":"Bartocci, Ezio","last_name":"Bartocci"},{"first_name":"Grégory","full_name":"Batt, Grégory","last_name":"Batt"},{"id":"3BDE25AA-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-3066-6941","first_name":"Hui","full_name":"Kong, Hui","last_name":"Kong"},{"first_name":"Radu","full_name":"Grosu, Radu","last_name":"Grosu"}],"alternative_title":["LNCS"],"day":"28","project":[{"name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"}],"acknowledgement":"This work was partly supported by the European Research Council (ERC) under grant 267989 (QUAREM), by the Austrian Science Fund (FWF) under grants S11402-N23, S11405-N23 and S11412-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award), and by the German Research Foundation (DFG) as part of the Transregional Collaborative Research Center “Automatic Verification and Analysis of Complex Systems” (SFB/TR 14 AVACS, http://www.avacs.org/).","ddc":["000"],"doi":"10.1007/978-3-319-26287-1_2","language":[{"iso":"eng"}],"article_processing_charge":"No","date_published":"2015-11-28T00:00:00Z","_id":"1605","abstract":[{"lang":"eng","text":"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."}],"file":[{"creator":"dernst","file_size":1053207,"file_name":"2015_LNCS_Bogomolov.pdf","access_level":"open_access","date_updated":"2020-07-14T12:45:05Z","checksum":"3aab260f3f34641d622030ba22645b3e","relation":"main_file","file_id":"7851","content_type":"application/pdf","date_created":"2020-05-15T08:43:19Z"}],"oa":1,"publication_status":"published","volume":9434,"file_date_updated":"2020-07-14T12:45:05Z","year":"2015","oa_version":"Submitted Version","has_accepted_license":"1","publist_id":"5561","scopus_import":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2021-01-12T06:51:56Z"},{"page":"281 - 286","date_created":"2018-12-11T11:52:59Z","month":"11","publisher":"Springer Nature","status":"public","intvolume":"      9333","publication":"6th International Conference","department":[{"_id":"ToHe"}],"quality_controlled":"1","title":"Runtime verification for hybrid analysis tools","conference":{"name":"RV: Runtime Verification","start_date":"2015-09-22","end_date":"2015-09-25","location":"Vienna, Austria"},"citation":{"short":"L. Nguyen, C. Schilling, S. Bogomolov, T. Johnson, in:, 6th International Conference, Springer Nature, 2015, pp. 281–286.","ama":"Nguyen L, Schilling C, Bogomolov S, Johnson T. Runtime verification for hybrid analysis tools. In: <i>6th International Conference</i>. Vol 9333. Springer Nature; 2015:281-286. doi:<a href=\"https://doi.org/10.1007/978-3-319-23820-3_19\">10.1007/978-3-319-23820-3_19</a>","apa":"Nguyen, L., Schilling, C., Bogomolov, S., &#38; Johnson, T. (2015). Runtime verification for hybrid analysis tools. In <i>6th International Conference</i> (Vol. 9333, pp. 281–286). Vienna, Austria: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-319-23820-3_19\">https://doi.org/10.1007/978-3-319-23820-3_19</a>","chicago":"Nguyen, Luan, Christian Schilling, Sergiy Bogomolov, and Taylor Johnson. “Runtime Verification for Hybrid Analysis Tools.” In <i>6th International Conference</i>, 9333:281–86. Springer Nature, 2015. <a href=\"https://doi.org/10.1007/978-3-319-23820-3_19\">https://doi.org/10.1007/978-3-319-23820-3_19</a>.","ieee":"L. Nguyen, C. Schilling, S. Bogomolov, and T. Johnson, “Runtime verification for hybrid analysis tools,” in <i>6th International Conference</i>, Vienna, Austria, 2015, vol. 9333, pp. 281–286.","ista":"Nguyen L, Schilling C, Bogomolov S, Johnson T. 2015. Runtime verification for hybrid analysis tools. 6th International Conference. RV: Runtime Verification, LNCS, vol. 9333, 281–286.","mla":"Nguyen, Luan, et al. “Runtime Verification for Hybrid Analysis Tools.” <i>6th International Conference</i>, vol. 9333, Springer Nature, 2015, pp. 281–86, doi:<a href=\"https://doi.org/10.1007/978-3-319-23820-3_19\">10.1007/978-3-319-23820-3_19</a>."},"ec_funded":1,"author":[{"last_name":"Nguyen","first_name":"Luan","full_name":"Nguyen, Luan"},{"last_name":"Schilling","full_name":"Schilling, Christian","first_name":"Christian"},{"orcid":"0000-0002-0686-0365","id":"369D9A44-F248-11E8-B48F-1D18A9856A87","last_name":"Bogomolov","full_name":"Bogomolov, Sergiy","first_name":"Sergiy"},{"last_name":"Johnson","full_name":"Johnson, Taylor","first_name":"Taylor"}],"type":"conference","alternative_title":["LNCS"],"day":"15","project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"name":"The Wittgenstein Prize","grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"}],"doi":"10.1007/978-3-319-23820-3_19","language":[{"iso":"eng"}],"article_processing_charge":"No","_id":"1606","date_published":"2015-11-15T00:00:00Z","abstract":[{"text":"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.","lang":"eng"}],"publication_status":"published","volume":9333,"oa_version":"None","year":"2015","publist_id":"5562","publication_identifier":{"isbn":["978-3-319-23819-7"]},"scopus_import":"1","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","date_updated":"2022-02-01T14:52:59Z"},{"scopus_import":1,"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","date_updated":"2023-09-07T12:01:59Z","oa_version":"Preprint","year":"2015","publist_id":"5560","volume":9206,"oa":1,"main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1504.07384"}],"publication_status":"published","_id":"1607","date_published":"2015-07-16T00:00:00Z","abstract":[{"lang":"eng","text":"We consider the core algorithmic problems related to verification of systems with respect to three classical quantitative properties, namely, the mean-payoff property, the ratio property, and the minimum initial credit for energy property. The algorithmic problem given a graph and a quantitative property asks to compute the optimal value (the infimum value over all traces) from every node of the graph. We consider graphs with constant treewidth, and it is well-known that the control-flow graphs of most programs have constant treewidth. Let n denote the number of nodes of a graph, m the number of edges (for constant treewidth graphs m=O(n)) and W the largest absolute value of the weights. Our main theoretical results are as follows. First, for constant treewidth graphs we present an algorithm that approximates the mean-payoff value within a multiplicative factor of ϵ in time O(n⋅log(n/ϵ)) and linear space, as compared to the classical algorithms that require quadratic time. Second, for the ratio property we present an algorithm that for constant treewidth graphs works in time O(n⋅log(|a⋅b|))=O(n⋅log(n⋅W)), when the output is ab, as compared to the previously best known algorithm with running time O(n2⋅log(n⋅W)). Third, for the minimum initial credit problem we show that (i) for general graphs the problem can be solved in O(n2⋅m) time and the associated decision problem can be solved in O(n⋅m) time, improving the previous known O(n3⋅m⋅log(n⋅W)) and O(n2⋅m) bounds, respectively; and (ii) for constant treewidth graphs we present an algorithm that requires O(n⋅logn) time, improving the previous known O(n4⋅log(n⋅W)) bound. We have implemented some of our algorithms and show that they present a significant speedup on standard benchmarks."}],"doi":"10.1007/978-3-319-21690-4_9","language":[{"iso":"eng"}],"project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"related_material":{"record":[{"status":"public","relation":"earlier_version","id":"5430"},{"status":"public","id":"5437","relation":"earlier_version"},{"status":"public","relation":"dissertation_contains","id":"821"}]},"acknowledgement":"The research was partly supported by Austrian Science Fund (FWF) Grant No P23499- N23, FWF NFN Grant No S11407-N23 (RiSE/SHiNE), ERC Start grant (279307: Graph Games), and Microsoft faculty fellows award.","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"orcid":"0000-0003-4783-0389","id":"3B699956-F248-11E8-B48F-1D18A9856A87","full_name":"Ibsen-Jensen, Rasmus","first_name":"Rasmus","last_name":"Ibsen-Jensen"},{"first_name":"Andreas","full_name":"Pavlogiannis, Andreas","last_name":"Pavlogiannis","orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87"}],"type":"conference","alternative_title":["LNCS"],"day":"16","title":"Faster algorithms for quantitative verification in constant treewidth graphs","conference":{"location":"San Francisco, CA, USA","start_date":"2015-07-18","end_date":"2015-07-24","name":"CAV: Computer Aided Verification"},"citation":{"ama":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. Faster algorithms for quantitative verification in constant treewidth graphs. In: Vol 9206. Springer; 2015:140-157. doi:<a href=\"https://doi.org/10.1007/978-3-319-21690-4_9\">10.1007/978-3-319-21690-4_9</a>","apa":"Chatterjee, K., Ibsen-Jensen, R., &#38; Pavlogiannis, A. (2015). Faster algorithms for quantitative verification in constant treewidth graphs (Vol. 9206, pp. 140–157). Presented at the CAV: Computer Aided Verification, San Francisco, CA, USA: Springer. <a href=\"https://doi.org/10.1007/978-3-319-21690-4_9\">https://doi.org/10.1007/978-3-319-21690-4_9</a>","short":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, in:, Springer, 2015, pp. 140–157.","mla":"Chatterjee, Krishnendu, et al. <i>Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs</i>. Vol. 9206, Springer, 2015, pp. 140–57, doi:<a href=\"https://doi.org/10.1007/978-3-319-21690-4_9\">10.1007/978-3-319-21690-4_9</a>.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. “Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs,” 9206:140–57. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-319-21690-4_9\">https://doi.org/10.1007/978-3-319-21690-4_9</a>.","ieee":"K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, “Faster algorithms for quantitative verification in constant treewidth graphs,” presented at the CAV: Computer Aided Verification, San Francisco, CA, USA, 2015, vol. 9206, pp. 140–157.","ista":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2015. Faster algorithms for quantitative verification in constant treewidth graphs. CAV: Computer Aided Verification, LNCS, vol. 9206, 140–157."},"ec_funded":1,"status":"public","intvolume":"      9206","quality_controlled":"1","department":[{"_id":"KrCh"}],"publisher":"Springer","date_created":"2018-12-11T11:52:59Z","month":"07","page":"140 - 157"},{"article_processing_charge":"No","date_published":"2015-06-20T00:00:00Z","_id":"1609","abstract":[{"lang":"eng","text":"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."}],"oa":1,"main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1502.04844"}],"publication_status":"published","volume":9135,"year":"2015","oa_version":"Preprint","publist_id":"5557","publication_identifier":{"isbn":["978-3-662-47665-9"]},"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","date_updated":"2022-02-01T15:04:44Z","scopus_import":"1","page":"108 - 120","date_created":"2018-12-11T11:53:00Z","month":"06","publisher":"Springer Nature","intvolume":"      9135","status":"public","quality_controlled":"1","department":[{"_id":"KrCh"}],"publication":"42nd International Colloquium","conference":{"location":"Kyoto, Japan","name":"ICALP: Automata, Languages and Programming","end_date":"2015-07-10","start_date":"2015-07-06"},"title":"The complexity of synthesis from probabilistic components","ec_funded":1,"citation":{"short":"K. Chatterjee, L. Doyen, M. Vardi, in:, 42nd International Colloquium, Springer Nature, 2015, pp. 108–120.","apa":"Chatterjee, K., Doyen, L., &#38; Vardi, M. (2015). The complexity of synthesis from probabilistic components. In <i>42nd International Colloquium</i> (Vol. 9135, pp. 108–120). Kyoto, Japan: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-662-47666-6_9\">https://doi.org/10.1007/978-3-662-47666-6_9</a>","ama":"Chatterjee K, Doyen L, Vardi M. The complexity of synthesis from probabilistic components. In: <i>42nd International Colloquium</i>. Vol 9135. Springer Nature; 2015:108-120. doi:<a href=\"https://doi.org/10.1007/978-3-662-47666-6_9\">10.1007/978-3-662-47666-6_9</a>","ista":"Chatterjee K, Doyen L, Vardi M. 2015. The complexity of synthesis from probabilistic components. 42nd International Colloquium. ICALP: Automata, Languages and Programming, LNCS, vol. 9135, 108–120.","ieee":"K. Chatterjee, L. Doyen, and M. Vardi, “The complexity of synthesis from probabilistic components,” in <i>42nd International Colloquium</i>, Kyoto, Japan, 2015, vol. 9135, pp. 108–120.","chicago":"Chatterjee, Krishnendu, Laurent Doyen, and Moshe Vardi. “The Complexity of Synthesis from Probabilistic Components.” In <i>42nd International Colloquium</i>, 9135:108–20. Springer Nature, 2015. <a href=\"https://doi.org/10.1007/978-3-662-47666-6_9\">https://doi.org/10.1007/978-3-662-47666-6_9</a>.","mla":"Chatterjee, Krishnendu, et al. “The Complexity of Synthesis from Probabilistic Components.” <i>42nd International Colloquium</i>, vol. 9135, Springer Nature, 2015, pp. 108–20, doi:<a href=\"https://doi.org/10.1007/978-3-662-47666-6_9\">10.1007/978-3-662-47666-6_9</a>."},"alternative_title":["LNCS"],"type":"conference","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee"},{"last_name":"Doyen","first_name":"Laurent","full_name":"Doyen, Laurent"},{"last_name":"Vardi","first_name":"Moshe","full_name":"Vardi, Moshe"}],"day":"20","acknowledgement":"This research was supported by Austrian Science Fund (FWF) Grant No P23499- N23, FWF NFN Grant No S11407-N23 (SHiNE), ERC Start grant (279307: Graph Games), EU FP7 Project Cassting, NSF grants CNS 1049862 and CCF-1139011, by NSF Expeditions in Computing project “ExCAPE: Expeditions in Computer Augmented Program Engineering”, by BSF grant 9800096, and by gift from Intel.","project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Game Theory","grant_number":"S11407"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"doi":"10.1007/978-3-662-47666-6_9","language":[{"iso":"eng"}]},{"publisher":"Springer Nature","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"quality_controlled":"1","publication":"42nd International Colloquium","status":"public","intvolume":"      9135","page":"121 - 133","month":"07","date_created":"2018-12-11T11:53:01Z","related_material":{"record":[{"id":"465","relation":"later_version","status":"public"},{"status":"public","id":"5438","relation":"earlier_version"}]},"project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11407","name":"Game Theory"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"}],"language":[{"iso":"eng"}],"doi":"10.1007/978-3-662-47666-6_10","ec_funded":1,"citation":{"chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Rasmus Ibsen-Jensen, and Jan Otop. “Edit Distance for Pushdown Automata.” In <i>42nd International Colloquium</i>, 9135:121–33. Springer Nature, 2015. <a href=\"https://doi.org/10.1007/978-3-662-47666-6_10\">https://doi.org/10.1007/978-3-662-47666-6_10</a>.","ieee":"K. Chatterjee, T. A. Henzinger, R. Ibsen-Jensen, and J. Otop, “Edit distance for pushdown automata,” in <i>42nd International Colloquium</i>, Kyoto, Japan, 2015, vol. 9135, no. Part II, pp. 121–133.","ista":"Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. 2015. Edit distance for pushdown automata. 42nd International Colloquium. ICALP: Automata, Languages and Programming, LNCS, vol. 9135, 121–133.","mla":"Chatterjee, Krishnendu, et al. “Edit Distance for Pushdown Automata.” <i>42nd International Colloquium</i>, vol. 9135, no. Part II, Springer Nature, 2015, pp. 121–33, doi:<a href=\"https://doi.org/10.1007/978-3-662-47666-6_10\">10.1007/978-3-662-47666-6_10</a>.","short":"K. Chatterjee, T.A. Henzinger, R. Ibsen-Jensen, J. Otop, in:, 42nd International Colloquium, Springer Nature, 2015, pp. 121–133.","ama":"Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. Edit distance for pushdown automata. In: <i>42nd International Colloquium</i>. Vol 9135. Springer Nature; 2015:121-133. doi:<a href=\"https://doi.org/10.1007/978-3-662-47666-6_10\">10.1007/978-3-662-47666-6_10</a>","apa":"Chatterjee, K., Henzinger, T. A., Ibsen-Jensen, R., &#38; Otop, J. (2015). Edit distance for pushdown automata. In <i>42nd International Colloquium</i> (Vol. 9135, pp. 121–133). Kyoto, Japan: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-662-47666-6_10\">https://doi.org/10.1007/978-3-662-47666-6_10</a>"},"conference":{"end_date":"2015-07-10","start_date":"2015-07-06","name":"ICALP: Automata, Languages and Programming","location":"Kyoto, Japan"},"title":"Edit distance for pushdown automata","day":"01","alternative_title":["LNCS"],"type":"conference","author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0003-4783-0389","id":"3B699956-F248-11E8-B48F-1D18A9856A87","first_name":"Rasmus","full_name":"Ibsen-Jensen, Rasmus","last_name":"Ibsen-Jensen"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","full_name":"Otop, Jan","last_name":"Otop"}],"publication_status":"published","oa":1,"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1504.08259"}],"volume":9135,"pubrep_id":"321","arxiv":1,"issue":"Part II","article_processing_charge":"No","_id":"1610","date_published":"2015-07-01T00:00:00Z","abstract":[{"lang":"eng","text":"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."}],"date_updated":"2023-02-23T12:26:24Z","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","external_id":{"arxiv":["1504.08259"]},"scopus_import":"1","publication_identifier":{"isbn":["978-3-662-47665-9"]},"publist_id":"5556","year":"2015","oa_version":"None"},{"publisher":"Wiley","quality_controlled":"1","department":[{"_id":"HaJa"}],"publication":"Protein Science","status":"public","intvolume":"        24","page":"1412 - 1422","month":"09","date_created":"2018-12-11T11:53:01Z","pmid":1,"project":[{"_id":"255BFFFA-B435-11E9-9278-68D0E5697425","grant_number":"RGY0084/2012","name":"In situ real-time imaging of neurotransmitter signaling using designer optical sensors (HFSP Young Investigator)"}],"language":[{"iso":"eng"}],"doi":"10.1002/pro.2721","citation":{"short":"J. Whitfield, W. Zhang, M. Herde, B. Clifton, J. Radziejewski, H.L. Janovjak, C. Henneberger, C. Jackson, Protein Science 24 (2015) 1412–1422.","ama":"Whitfield J, Zhang W, Herde M, et al. Construction of a robust and sensitive arginine biosensor through ancestral protein reconstruction. <i>Protein Science</i>. 2015;24(9):1412-1422. doi:<a href=\"https://doi.org/10.1002/pro.2721\">10.1002/pro.2721</a>","apa":"Whitfield, J., Zhang, W., Herde, M., Clifton, B., Radziejewski, J., Janovjak, H. L., … Jackson, C. (2015). Construction of a robust and sensitive arginine biosensor through ancestral protein reconstruction. <i>Protein Science</i>. Wiley. <a href=\"https://doi.org/10.1002/pro.2721\">https://doi.org/10.1002/pro.2721</a>","chicago":"Whitfield, Jason, William Zhang, Michel Herde, Ben Clifton, Johanna Radziejewski, Harald L Janovjak, Christian Henneberger, and Colin Jackson. “Construction of a Robust and Sensitive Arginine Biosensor through Ancestral Protein Reconstruction.” <i>Protein Science</i>. Wiley, 2015. <a href=\"https://doi.org/10.1002/pro.2721\">https://doi.org/10.1002/pro.2721</a>.","ieee":"J. Whitfield <i>et al.</i>, “Construction of a robust and sensitive arginine biosensor through ancestral protein reconstruction,” <i>Protein Science</i>, vol. 24, no. 9. Wiley, pp. 1412–1422, 2015.","ista":"Whitfield J, Zhang W, Herde M, Clifton B, Radziejewski J, Janovjak HL, Henneberger C, Jackson C. 2015. Construction of a robust and sensitive arginine biosensor through ancestral protein reconstruction. Protein Science. 24(9), 1412–1422.","mla":"Whitfield, Jason, et al. “Construction of a Robust and Sensitive Arginine Biosensor through Ancestral Protein Reconstruction.” <i>Protein Science</i>, vol. 24, no. 9, Wiley, 2015, pp. 1412–22, doi:<a href=\"https://doi.org/10.1002/pro.2721\">10.1002/pro.2721</a>."},"title":"Construction of a robust and sensitive arginine biosensor through ancestral protein reconstruction","day":"01","type":"journal_article","author":[{"last_name":"Whitfield","full_name":"Whitfield, Jason","first_name":"Jason"},{"last_name":"Zhang","first_name":"William","full_name":"Zhang, William"},{"full_name":"Herde, Michel","first_name":"Michel","last_name":"Herde"},{"full_name":"Clifton, Ben","first_name":"Ben","last_name":"Clifton"},{"last_name":"Radziejewski","first_name":"Johanna","full_name":"Radziejewski, Johanna"},{"full_name":"Janovjak, Harald L","first_name":"Harald L","last_name":"Janovjak","id":"33BA6C30-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8023-9315"},{"last_name":"Henneberger","first_name":"Christian","full_name":"Henneberger, Christian"},{"first_name":"Colin","full_name":"Jackson, Colin","last_name":"Jackson"}],"publication_status":"published","main_file_link":[{"url":"https://www.ncbi.nlm.nih.gov/pmc/articles/PMC4570536/","open_access":"1"}],"oa":1,"volume":24,"issue":"9","_id":"1611","date_published":"2015-09-01T00:00:00Z","abstract":[{"text":"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 &quot;core&quot; 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.","lang":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2021-01-12T06:52:00Z","scopus_import":1,"external_id":{"pmid":["26061224"]},"publist_id":"5555","year":"2015","oa_version":"Submitted Version"},{"oa_version":"Published Version","year":"2015","has_accepted_license":"1","publist_id":"5552","scopus_import":1,"external_id":{"pmid":["25583495"]},"date_updated":"2021-01-12T06:52:01Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","issue":"4","_id":"1614","date_published":"2015-01-27T00:00:00Z","abstract":[{"text":"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. ","lang":"eng"}],"file":[{"date_created":"2019-01-17T07:52:40Z","relation":"main_file","file_id":"5838","content_type":"application/pdf","checksum":"6703309a1f58493cf5a704211fb6ebed","access_level":"open_access","date_updated":"2020-07-14T12:45:07Z","file_size":1280860,"creator":"dernst","file_name":"2015_PNAS_Strueber.pdf"}],"oa":1,"publication_status":"published","volume":112,"file_date_updated":"2020-07-14T12:45:07Z","title":"Strength and duration of perisomatic GABAergic inhibition depend on distance between synaptically connected cells","citation":{"short":"M. Strüber, P.M. Jonas, M. Bartos, PNAS 112 (2015) 1220–1225.","ama":"Strüber M, Jonas PM, Bartos M. Strength and duration of perisomatic GABAergic inhibition depend on distance between synaptically connected cells. <i>PNAS</i>. 2015;112(4):1220-1225. doi:<a href=\"https://doi.org/10.1073/pnas.1412996112\">10.1073/pnas.1412996112</a>","apa":"Strüber, M., Jonas, P. M., &#38; Bartos, M. (2015). Strength and duration of perisomatic GABAergic inhibition depend on distance between synaptically connected cells. <i>PNAS</i>. National Academy of Sciences. <a href=\"https://doi.org/10.1073/pnas.1412996112\">https://doi.org/10.1073/pnas.1412996112</a>","chicago":"Strüber, Michael, Peter M Jonas, and Marlene Bartos. “Strength and Duration of Perisomatic GABAergic Inhibition Depend on Distance between Synaptically Connected Cells.” <i>PNAS</i>. National Academy of Sciences, 2015. <a href=\"https://doi.org/10.1073/pnas.1412996112\">https://doi.org/10.1073/pnas.1412996112</a>.","ista":"Strüber M, Jonas PM, Bartos M. 2015. Strength and duration of perisomatic GABAergic inhibition depend on distance between synaptically connected cells. PNAS. 112(4), 1220–1225.","ieee":"M. Strüber, P. M. Jonas, and M. Bartos, “Strength and duration of perisomatic GABAergic inhibition depend on distance between synaptically connected cells,” <i>PNAS</i>, vol. 112, no. 4. National Academy of Sciences, pp. 1220–1225, 2015.","mla":"Strüber, Michael, et al. “Strength and Duration of Perisomatic GABAergic Inhibition Depend on Distance between Synaptically Connected Cells.” <i>PNAS</i>, vol. 112, no. 4, National Academy of Sciences, 2015, pp. 1220–25, doi:<a href=\"https://doi.org/10.1073/pnas.1412996112\">10.1073/pnas.1412996112</a>."},"ec_funded":1,"type":"journal_article","author":[{"last_name":"Strüber","first_name":"Michael","full_name":"Strüber, Michael"},{"first_name":"Peter M","full_name":"Jonas, Peter M","last_name":"Jonas","id":"353C1B58-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5001-4804"},{"full_name":"Bartos, Marlene","first_name":"Marlene","last_name":"Bartos"}],"day":"27","project":[{"_id":"25C26B1E-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Mechanisms of transmitter release at GABAergic synapses","grant_number":"P24909-B24"},{"call_identifier":"FP7","_id":"25C0F108-B435-11E9-9278-68D0E5697425","grant_number":"268548","name":"Nanophysiology of fast-spiking, parvalbumin-expressing GABAergic interneurons"}],"pmid":1,"doi":"10.1073/pnas.1412996112","ddc":["570"],"language":[{"iso":"eng"}],"page":"1220 - 1225","date_created":"2018-12-11T11:53:02Z","month":"01","publisher":"National Academy of Sciences","status":"public","intvolume":"       112","publication":"PNAS","department":[{"_id":"PeJo"}],"quality_controlled":"1"},{"type":"journal_article","author":[{"first_name":"Julian L","full_name":"Julian Fischer","last_name":"Fischer","id":"2C12A0B0-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-0479-558X"},{"last_name":"Grün","first_name":"Günther","full_name":"Grün, Günther"}],"year":"2015","publist_id":"5958","day":"01","title":"Finite speed of propagation and waiting times for the stochastic porous medium equation: A unifying approach","citation":{"chicago":"Fischer, Julian L, and Günther Grün. “Finite Speed of Propagation and Waiting Times for the Stochastic Porous Medium Equation: A Unifying Approach.” <i>SIAM Journal on Mathematical Analysis</i>. Society for Industrial and Applied Mathematics , 2015. <a href=\"https://doi.org/10.1137/140960578\">https://doi.org/10.1137/140960578</a>.","ista":"Fischer JL, Grün G. 2015. Finite speed of propagation and waiting times for the stochastic porous medium equation: A unifying approach. SIAM Journal on Mathematical Analysis. 47(1), 825–854.","ieee":"J. L. Fischer and G. Grün, “Finite speed of propagation and waiting times for the stochastic porous medium equation: A unifying approach,” <i>SIAM Journal on Mathematical Analysis</i>, vol. 47, no. 1. Society for Industrial and Applied Mathematics , pp. 825–854, 2015.","mla":"Fischer, Julian L., and Günther Grün. “Finite Speed of Propagation and Waiting Times for the Stochastic Porous Medium Equation: A Unifying Approach.” <i>SIAM Journal on Mathematical Analysis</i>, vol. 47, no. 1, Society for Industrial and Applied Mathematics , 2015, pp. 825–54, doi:<a href=\"https://doi.org/10.1137/140960578\">10.1137/140960578</a>.","short":"J.L. Fischer, G. Grün, SIAM Journal on Mathematical Analysis 47 (2015) 825–854.","ama":"Fischer JL, Grün G. Finite speed of propagation and waiting times for the stochastic porous medium equation: A unifying approach. <i>SIAM Journal on Mathematical Analysis</i>. 2015;47(1):825-854. doi:<a href=\"https://doi.org/10.1137/140960578\">10.1137/140960578</a>","apa":"Fischer, J. L., &#38; Grün, G. (2015). Finite speed of propagation and waiting times for the stochastic porous medium equation: A unifying approach. <i>SIAM Journal on Mathematical Analysis</i>. Society for Industrial and Applied Mathematics . <a href=\"https://doi.org/10.1137/140960578\">https://doi.org/10.1137/140960578</a>"},"doi":"10.1137/140960578","date_updated":"2021-01-12T06:49:48Z","acknowledgement":"The first author has been supported by the Lithuanian-Swiss co- operation program under the project agreement No. CH-SMM-01/0.","date_created":"2018-12-11T11:51:18Z","_id":"1311","date_published":"2015-01-01T00:00:00Z","abstract":[{"text":"In this paper, we develop an energy method to study finite speed of propagation and waiting time phenomena for the stochastic porous media equation with linear multiplicative noise in up to three spatial dimensions. Based on a novel iteration technique and on stochastic counterparts of weighted integral estimates used in the deterministic setting, we formulate a sufficient criterion on the growth of initial data which locally guarantees a waiting time phenomenon to occur almost surely. Up to a logarithmic factor, this criterion coincides with the optimal criterion known from the deterministic setting. Our technique can be modified to prove finite speed of propagation as well.","lang":"eng"}],"month":"01","extern":1,"issue":"1","page":"825 - 854","intvolume":"        47","status":"public","volume":47,"publication":"SIAM Journal on Mathematical Analysis","quality_controlled":0,"publication_status":"published","publisher":"Society for Industrial and Applied Mathematics "},{"citation":{"mla":"Fischer, Julian L. “Estimates on Front Propagation for Nonlinear Higher-Order Parabolic Equations: An Algorithmic Approach.” <i>Interfaces and Free Boundaries</i>, vol. 17, no. 1, European Mathematical Society Publishing House, 2015, pp. 1–20, doi:<a href=\"https://doi.org/10.4171/IFB/331\">10.4171/IFB/331</a>.","ieee":"J. L. Fischer, “Estimates on front propagation for nonlinear higher-order parabolic equations: An algorithmic approach,” <i>Interfaces and Free Boundaries</i>, vol. 17, no. 1. European Mathematical Society Publishing House, pp. 1–20, 2015.","ista":"Fischer JL. 2015. Estimates on front propagation for nonlinear higher-order parabolic equations: An algorithmic approach. Interfaces and Free Boundaries. 17(1), 1–20.","chicago":"Fischer, Julian L. “Estimates on Front Propagation for Nonlinear Higher-Order Parabolic Equations: An Algorithmic Approach.” <i>Interfaces and Free Boundaries</i>. European Mathematical Society Publishing House, 2015. <a href=\"https://doi.org/10.4171/IFB/331\">https://doi.org/10.4171/IFB/331</a>.","apa":"Fischer, J. L. (2015). Estimates on front propagation for nonlinear higher-order parabolic equations: An algorithmic approach. <i>Interfaces and Free Boundaries</i>. European Mathematical Society Publishing House. <a href=\"https://doi.org/10.4171/IFB/331\">https://doi.org/10.4171/IFB/331</a>","ama":"Fischer JL. Estimates on front propagation for nonlinear higher-order parabolic equations: An algorithmic approach. <i>Interfaces and Free Boundaries</i>. 2015;17(1):1-20. doi:<a href=\"https://doi.org/10.4171/IFB/331\">10.4171/IFB/331</a>","short":"J.L. Fischer, Interfaces and Free Boundaries 17 (2015) 1–20."},"title":"Estimates on front propagation for nonlinear higher-order parabolic equations: An algorithmic approach","publist_id":"5956","day":"01","year":"2015","author":[{"orcid":"0000-0002-0479-558X","id":"2C12A0B0-F248-11E8-B48F-1D18A9856A87","first_name":"Julian L","full_name":"Julian Fischer","last_name":"Fischer"}],"type":"journal_article","acknowledgement":"This research was supported by the Lithuanian-Swiss cooperation program under the project agreement No.  CH-SMM-01/0.","date_updated":"2021-01-12T06:49:48Z","doi":"10.4171/IFB/331","page":"1 - 20","issue":"1","extern":1,"month":"01","abstract":[{"lang":"eng","text":"We present an algorithm for the derivation of lower bounds on support propagation for a certain class of nonlinear parabolic equations. We proceed by combining the ideas in some recent papers by the author with the algorithmic construction of entropies due to Jüngel and Matthes, reducing the problem to a quantifier elimination problem. Due to its complexity, the quantifier elimination problem cannot be solved by present exact algorithms. However, by tackling the quantifier elimination problem numerically, in the case of the thin-film equation we are able to improve recent results by the author in the regime of strong slippage n ∈ (1, 2). For certain second-order doubly nonlinear parabolic equations, we are able to extend the known lower bounds on free boundary propagation to the case of irregular oscillatory initial data. Finally, we apply our method to a sixth-order quantum drift-diffusion equation, resulting in an upper bound on the time which it takes for the support to reach every point in the domain."}],"_id":"1313","date_published":"2015-01-01T00:00:00Z","date_created":"2018-12-11T11:51:19Z","publisher":"European Mathematical Society Publishing House","publication_status":"published","quality_controlled":0,"publication":"Interfaces and Free Boundaries","volume":17,"status":"public","intvolume":"        17"},{"doi":"10.1137/140966654","date_updated":"2021-01-12T06:49:49Z","language":[{"iso":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","acknowledgement":"The research of the author was supported by the Lithuanian-Swiss cooperation program under the project agreement CH-SMM-01/0.","year":"2015","oa_version":"None","author":[{"id":"2C12A0B0-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-0479-558X","last_name":"Fischer","full_name":"Fischer, Julian L","first_name":"Julian L"}],"type":"journal_article","day":"01","publist_id":"5957","title":"A posteriori modeling error estimates for the assumption of perfect incompressibility in the Navier-Stokes equation","citation":{"apa":"Fischer, J. L. (2015). A posteriori modeling error estimates for the assumption of perfect incompressibility in the Navier-Stokes equation. <i>SIAM Journal on Numerical Analysis</i>. Society for Industrial and Applied Mathematics . <a href=\"https://doi.org/10.1137/140966654\">https://doi.org/10.1137/140966654</a>","ama":"Fischer JL. A posteriori modeling error estimates for the assumption of perfect incompressibility in the Navier-Stokes equation. <i>SIAM Journal on Numerical Analysis</i>. 2015;53(5):2178-2205. doi:<a href=\"https://doi.org/10.1137/140966654\">10.1137/140966654</a>","short":"J.L. Fischer, SIAM Journal on Numerical Analysis 53 (2015) 2178–2205.","mla":"Fischer, Julian L. “A Posteriori Modeling Error Estimates for the Assumption of Perfect Incompressibility in the Navier-Stokes Equation.” <i>SIAM Journal on Numerical Analysis</i>, vol. 53, no. 5, Society for Industrial and Applied Mathematics , 2015, pp. 2178–205, doi:<a href=\"https://doi.org/10.1137/140966654\">10.1137/140966654</a>.","ieee":"J. L. Fischer, “A posteriori modeling error estimates for the assumption of perfect incompressibility in the Navier-Stokes equation,” <i>SIAM Journal on Numerical Analysis</i>, vol. 53, no. 5. Society for Industrial and Applied Mathematics , pp. 2178–2205, 2015.","ista":"Fischer JL. 2015. A posteriori modeling error estimates for the assumption of perfect incompressibility in the Navier-Stokes equation. SIAM Journal on Numerical Analysis. 53(5), 2178–2205.","chicago":"Fischer, Julian L. “A Posteriori Modeling Error Estimates for the Assumption of Perfect Incompressibility in the Navier-Stokes Equation.” <i>SIAM Journal on Numerical Analysis</i>. Society for Industrial and Applied Mathematics , 2015. <a href=\"https://doi.org/10.1137/140966654\">https://doi.org/10.1137/140966654</a>."},"volume":53,"status":"public","intvolume":"        53","quality_controlled":"1","publication":"SIAM Journal on Numerical Analysis","publication_status":"published","publisher":"Society for Industrial and Applied Mathematics ","_id":"1314","abstract":[{"lang":"eng","text":"We derive a posteriori estimates for the modeling error caused by the assumption of perfect incompressibility in the incompressible Navier-Stokes equation: Real fluids are never perfectly incompressible but always feature at least some low amount of compressibility. Thus, their behavior is described by the compressible Navier-Stokes equation, the pressure being a steep function of the density. We rigorously estimate the difference between an approximate solution to the incompressible Navier-Stokes equation and any weak solution to the compressible Navier-Stokes equation in the sense of Lions (without assuming any additional regularity of solutions). Heuristics and numerical results suggest that our error estimates are of optimal order in the case of &quot;well-behaved&quot; flows and divergence-free approximations of the velocity field. Thus, we expect our estimates to justify the idealization of fluids as perfectly incompressible also in practical situations."}],"date_created":"2018-12-11T11:51:19Z","date_published":"2015-01-01T00:00:00Z","extern":"1","month":"01","issue":"5","page":"2178 - 2205"},{"volume":218,"intvolume":"       218","status":"public","quality_controlled":0,"publication":"Archive for Rational Mechanics and Analysis","publisher":"Springer","publication_status":"published","_id":"1316","date_created":"2018-12-11T11:51:20Z","date_published":"2015-10-01T00:00:00Z","abstract":[{"text":"In the present work we introduce the notion of a renormalized solution for reaction–diffusion systems with entropy-dissipating reactions. We establish the global existence of renormalized solutions. In the case of integrable reaction terms our notion of a renormalized solution reduces to the usual notion of a weak solution. Our existence result in particular covers all reaction–diffusion systems involving a single reversible reaction with mass-action kinetics and (possibly species-dependent) Fick-law diffusion; more generally, it covers the case of systems of reversible reactions with mass-action kinetics which satisfy the detailed balance condition. For such equations the existence of any kind of solution in general was an open problem, thereby motivating the study of renormalized solutions.","lang":"eng"}],"extern":1,"month":"10","issue":"1","page":"553 - 587","doi":"10.1007/s00205-015-0866-x","date_updated":"2021-01-12T06:49:50Z","acknowledgement":"This research was supported by the Lithuanian-Swiss cooperation program under the project agreement No. CH-SMM-01/0.","year":"2015","author":[{"last_name":"Fischer","first_name":"Julian L","full_name":"Julian Fischer","orcid":"0000-0002-0479-558X","id":"2C12A0B0-F248-11E8-B48F-1D18A9856A87"}],"type":"journal_article","publist_id":"5955","day":"01","title":"Global existence of renormalized solutions to entropy-dissipating reaction–diffusion systems","citation":{"chicago":"Fischer, Julian L. “Global Existence of Renormalized Solutions to Entropy-Dissipating Reaction–Diffusion Systems.” <i>Archive for Rational Mechanics and Analysis</i>. Springer, 2015. <a href=\"https://doi.org/10.1007/s00205-015-0866-x\">https://doi.org/10.1007/s00205-015-0866-x</a>.","ieee":"J. L. Fischer, “Global existence of renormalized solutions to entropy-dissipating reaction–diffusion systems,” <i>Archive for Rational Mechanics and Analysis</i>, vol. 218, no. 1. Springer, pp. 553–587, 2015.","ista":"Fischer JL. 2015. Global existence of renormalized solutions to entropy-dissipating reaction–diffusion systems. Archive for Rational Mechanics and Analysis. 218(1), 553–587.","mla":"Fischer, Julian L. “Global Existence of Renormalized Solutions to Entropy-Dissipating Reaction–Diffusion Systems.” <i>Archive for Rational Mechanics and Analysis</i>, vol. 218, no. 1, Springer, 2015, pp. 553–87, doi:<a href=\"https://doi.org/10.1007/s00205-015-0866-x\">10.1007/s00205-015-0866-x</a>.","short":"J.L. Fischer, Archive for Rational Mechanics and Analysis 218 (2015) 553–587.","ama":"Fischer JL. Global existence of renormalized solutions to entropy-dissipating reaction–diffusion systems. <i>Archive for Rational Mechanics and Analysis</i>. 2015;218(1):553-587. doi:<a href=\"https://doi.org/10.1007/s00205-015-0866-x\">10.1007/s00205-015-0866-x</a>","apa":"Fischer, J. L. (2015). Global existence of renormalized solutions to entropy-dissipating reaction–diffusion systems. <i>Archive for Rational Mechanics and Analysis</i>. Springer. <a href=\"https://doi.org/10.1007/s00205-015-0866-x\">https://doi.org/10.1007/s00205-015-0866-x</a>"}},{"year":"2015","oa_version":"None","article_type":"original","publication_identifier":{"eissn":["1748-3395"],"issn":["1748-3387"]},"date_updated":"2023-08-07T12:55:46Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","external_id":{"pmid":["26595335"]},"scopus_import":"1","abstract":[{"text":"The chemical behaviour of molecules can be significantly modified by confinement to volumes comparable to the dimensions of the molecules. Although such confined spaces can be found in various nanostructured materials, such as zeolites, nanoporous organic frameworks and colloidal nanocrystal assemblies, the slow diffusion of molecules in and out of these materials has greatly hampered studying the effect of confinement on their physicochemical properties. Here, we show that this diffusion limitation can be overcome by reversibly creating and destroying confined environments by means of ultraviolet and visible light irradiation. We use colloidal nanocrystals functionalized with light-responsive ligands that readily self-assemble and trap various molecules from the surrounding bulk solution. Once trapped, these molecules can undergo chemical reactions with increased rates and with stereoselectivities significantly different from those in bulk solution. Illumination with visible light disassembles these nanoflasks, releasing the product in solution and thereby establishes a catalytic cycle. These dynamic nanoflasks can be useful for studying chemical reactivities in confined environments and for synthesizing molecules that are otherwise hard to achieve in bulk solution.","lang":"eng"}],"_id":"13392","date_published":"2015-11-23T00:00:00Z","article_processing_charge":"No","volume":11,"publication_status":"published","author":[{"last_name":"Zhao","full_name":"Zhao, Hui","first_name":"Hui"},{"first_name":"Soumyo","full_name":"Sen, Soumyo","last_name":"Sen"},{"full_name":"Udayabhaskararao, T.","first_name":"T.","last_name":"Udayabhaskararao"},{"last_name":"Sawczyk","full_name":"Sawczyk, Michał","first_name":"Michał"},{"first_name":"Kristina","full_name":"Kučanda, Kristina","last_name":"Kučanda"},{"full_name":"Manna, Debasish","first_name":"Debasish","last_name":"Manna"},{"full_name":"Kundu, Pintu K.","first_name":"Pintu K.","last_name":"Kundu"},{"last_name":"Lee","first_name":"Ji-Woong","full_name":"Lee, Ji-Woong"},{"last_name":"Král","full_name":"Král, Petr","first_name":"Petr"},{"full_name":"Klajn, Rafal","first_name":"Rafal","last_name":"Klajn","id":"8e84690e-1e48-11ed-a02b-a1e6fb8bb53b"}],"type":"journal_article","day":"23","title":"Reversible trapping and reaction acceleration within dynamically self-assembling nanoflasks","citation":{"short":"H. Zhao, S. Sen, T. Udayabhaskararao, M. Sawczyk, K. Kučanda, D. Manna, P.K. Kundu, J.-W. Lee, P. Král, R. Klajn, Nature Nanotechnology 11 (2015) 82–88.","apa":"Zhao, H., Sen, S., Udayabhaskararao, T., Sawczyk, M., Kučanda, K., Manna, D., … Klajn, R. (2015). Reversible trapping and reaction acceleration within dynamically self-assembling nanoflasks. <i>Nature Nanotechnology</i>. Springer Nature. <a href=\"https://doi.org/10.1038/nnano.2015.256\">https://doi.org/10.1038/nnano.2015.256</a>","ama":"Zhao H, Sen S, Udayabhaskararao T, et al. Reversible trapping and reaction acceleration within dynamically self-assembling nanoflasks. <i>Nature Nanotechnology</i>. 2015;11:82-88. doi:<a href=\"https://doi.org/10.1038/nnano.2015.256\">10.1038/nnano.2015.256</a>","ista":"Zhao H, Sen S, Udayabhaskararao T, Sawczyk M, Kučanda K, Manna D, Kundu PK, Lee J-W, Král P, Klajn R. 2015. Reversible trapping and reaction acceleration within dynamically self-assembling nanoflasks. Nature Nanotechnology. 11, 82–88.","ieee":"H. Zhao <i>et al.</i>, “Reversible trapping and reaction acceleration within dynamically self-assembling nanoflasks,” <i>Nature Nanotechnology</i>, vol. 11. Springer Nature, pp. 82–88, 2015.","chicago":"Zhao, Hui, Soumyo Sen, T. Udayabhaskararao, Michał Sawczyk, Kristina Kučanda, Debasish Manna, Pintu K. Kundu, Ji-Woong Lee, Petr Král, and Rafal Klajn. “Reversible Trapping and Reaction Acceleration within Dynamically Self-Assembling Nanoflasks.” <i>Nature Nanotechnology</i>. Springer Nature, 2015. <a href=\"https://doi.org/10.1038/nnano.2015.256\">https://doi.org/10.1038/nnano.2015.256</a>.","mla":"Zhao, Hui, et al. “Reversible Trapping and Reaction Acceleration within Dynamically Self-Assembling Nanoflasks.” <i>Nature Nanotechnology</i>, vol. 11, Springer Nature, 2015, pp. 82–88, doi:<a href=\"https://doi.org/10.1038/nnano.2015.256\">10.1038/nnano.2015.256</a>."},"doi":"10.1038/nnano.2015.256","language":[{"iso":"eng"}],"keyword":["Electrical and Electronic Engineering","Condensed Matter Physics","General Materials Science","Biomedical Engineering","Atomic and Molecular Physics","and Optics","Bioengineering"],"pmid":1,"date_created":"2023-08-01T09:44:04Z","extern":"1","month":"11","page":"82-88","intvolume":"        11","status":"public","quality_controlled":"1","publication":"Nature Nanotechnology","publisher":"Springer Nature"}]