--- _id: '2265' abstract: - lang: eng text: Coordinated migration of newly-born neurons to their target territories is essential for correct neuronal circuit assembly in the developing brain. Although a cohort of signaling pathways has been implicated in the regulation of cortical projection neuron migration, the precise molecular mechanisms and how a balanced interplay of cell-autonomous and non-autonomous functions of candidate signaling molecules controls the discrete steps in the migration process, are just being revealed. In this chapter, I will focally review recent advances that improved our understanding of the cell-autonomous and possible cell-nonautonomous functions of the evolutionarily conserved LIS1/NDEL1-complex in regulating the sequential steps of cortical projection neuron migration. I will then elaborate on the emerging concept that the Reelin signaling pathway, acts exactly at precise stages in the course of cortical projection neuron migration. Lastly, I will discuss how finely tuned transcriptional programs and downstream effectors govern particular aspects in driving radial migration at discrete stages and how they regulate the precise positioning of cortical projection neurons in the developing cerebral cortex. alternative_title: - Advances in Experimental Medicine and Biology article_processing_charge: No author: - first_name: Simon full_name: Hippenmeyer, Simon id: 37B36620-F248-11E8-B48F-1D18A9856A87 last_name: Hippenmeyer orcid: 0000-0003-2279-1061 citation: ama: 'Hippenmeyer S. Molecular pathways controlling the sequential steps of cortical projection neuron migration. In: Nguyen L, ed. Cellular and Molecular Control of Neuronal Migration. Vol 800. Springer; 2014:1-24. doi:10.1007/978-94-007-7687-6_1' apa: Hippenmeyer, S. (2014). Molecular pathways controlling the sequential steps of cortical projection neuron migration. In L. Nguyen (Ed.), Cellular and Molecular Control of Neuronal Migration (Vol. 800, pp. 1–24). Springer. https://doi.org/10.1007/978-94-007-7687-6_1 chicago: Hippenmeyer, Simon. “Molecular Pathways Controlling the Sequential Steps of Cortical Projection Neuron Migration.” In Cellular and Molecular Control of Neuronal Migration, edited by Laurent Nguyen, 800:1–24. Springer, 2014. https://doi.org/10.1007/978-94-007-7687-6_1. ieee: S. Hippenmeyer, “Molecular pathways controlling the sequential steps of cortical projection neuron migration,” in Cellular and Molecular Control of Neuronal Migration, vol. 800, L. Nguyen, Ed. Springer, 2014, pp. 1–24. ista: 'Hippenmeyer S. 2014.Molecular pathways controlling the sequential steps of cortical projection neuron migration. In: Cellular and Molecular Control of Neuronal Migration. Advances in Experimental Medicine and Biology, vol. 800, 1–24.' mla: Hippenmeyer, Simon. “Molecular Pathways Controlling the Sequential Steps of Cortical Projection Neuron Migration.” Cellular and Molecular Control of Neuronal Migration, edited by Laurent Nguyen, vol. 800, Springer, 2014, pp. 1–24, doi:10.1007/978-94-007-7687-6_1. short: S. Hippenmeyer, in:, L. Nguyen (Ed.), Cellular and Molecular Control of Neuronal Migration, Springer, 2014, pp. 1–24. corr_author: '1' das_tickbox: '1' date_created: 2018-12-11T11:56:39Z date_published: 2014-01-01T00:00:00Z date_updated: 2026-07-07T13:04:40Z day: '01' department: - _id: SiHi doi: 10.1007/978-94-007-7687-6_1 editor: - first_name: Laurent full_name: Nguyen, Laurent last_name: Nguyen external_id: isi: - '000333646000002' fulldoi: https://doi.org/10.1007/978-94-007-7687-6_1 intvolume: ' 800' isi: 1 language: - iso: eng month: '01' oa_version: None page: 1 - 24 publication: Cellular and Molecular Control of Neuronal Migration publication_status: published publisher: Springer publist_id: '4679' quality_controlled: '1' scopus_import: '1' status: public title: Molecular pathways controlling the sequential steps of cortical projection neuron migration type: book_chapter user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 800 year: '2014' ... --- _id: '2027' abstract: - lang: eng text: We present a general framework for applying machine-learning algorithms to the verification of Markov decision processes (MDPs). The primary goal of these techniques is to improve performance by avoiding an exhaustive exploration of the state space. Our framework focuses on probabilistic reachability, which is a core property for verification, and is illustrated through two distinct instantiations. The first assumes that full knowledge of the MDP is available, and performs a heuristic-driven partial exploration of the model, yielding precise lower and upper bounds on the required probability. The second tackles the case where we may only sample the MDP, and yields probabilistic guarantees, again in terms of both the lower and upper bounds, which provides efficient stopping criteria for the approximation. The latter is the first extension of statistical model checking for unbounded properties inMDPs. In contrast with other related techniques, our approach is not restricted to time-bounded (finite-horizon) or discounted properties, nor does it assume any particular properties of the MDP. We also show how our methods extend to LTL objectives. We present experimental results showing the performance of our framework on several examples. acknowledgement: This research was funded in part by the European Research Council (ERC) under grant agreement 246967 (VERIWARE), by the EU FP7 project HIERATIC, by the Czech Science Foundation grant No P202/12/P612, by EPSRC project EP/K038575/1. alternative_title: - LNCS article_processing_charge: No arxiv: 1 author: - first_name: Tomáš full_name: Brázdil, Tomáš last_name: Brázdil - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Martin full_name: Chmelik, Martin id: 3624234E-F248-11E8-B48F-1D18A9856A87 last_name: Chmelik - first_name: Vojtěch full_name: Forejt, Vojtěch last_name: Forejt - first_name: Jan full_name: Kretinsky, Jan id: 44CEF464-F248-11E8-B48F-1D18A9856A87 last_name: Kretinsky orcid: 0000-0002-8122-2881 - first_name: Marta full_name: Kwiatkowska, Marta last_name: Kwiatkowska - first_name: David full_name: Parker, David last_name: Parker - first_name: Mateusz full_name: Ujma, Mateusz last_name: Ujma citation: ama: 'Brázdil T, Chatterjee K, Chmelik M, et al. Verification of Markov decision processes using learning algorithms. In: 12th International Symposium on Automated Technology for Verification and Analysis. Vol 8837. Springer; 2014:98-114. doi:10.1007/978-3-319-11936-6_8' apa: 'Brázdil, T., Chatterjee, K., Chmelik, M., Forejt, V., Kretinsky, J., Kwiatkowska, M., … Ujma, M. (2014). Verification of Markov decision processes using learning algorithms. In 12th International Symposium on Automated Technology for Verification and Analysis (Vol. 8837, pp. 98–114). Sydney, Australia: Springer. https://doi.org/10.1007/978-3-319-11936-6_8' chicago: Brázdil, Tomáš, Krishnendu Chatterjee, Martin Chmelik, Vojtěch Forejt, Jan Kretinsky, Marta Kwiatkowska, David Parker, and Mateusz Ujma. “Verification of Markov Decision Processes Using Learning Algorithms.” In 12th International Symposium on Automated Technology for Verification and Analysis, 8837:98–114. Springer, 2014. https://doi.org/10.1007/978-3-319-11936-6_8. ieee: T. Brázdil et al., “Verification of Markov decision processes using learning algorithms,” in 12th International Symposium on Automated Technology for Verification and Analysis, Sydney, Australia, 2014, vol. 8837, pp. 98–114. ista: 'Brázdil T, Chatterjee K, Chmelik M, Forejt V, Kretinsky J, Kwiatkowska M, Parker D, Ujma M. 2014. Verification of Markov decision processes using learning algorithms. 12th International Symposium on Automated Technology for Verification and Analysis. ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 8837, 98–114.' mla: Brázdil, Tomáš, et al. “Verification of Markov Decision Processes Using Learning Algorithms.” 12th International Symposium on Automated Technology for Verification and Analysis, vol. 8837, Springer, 2014, pp. 98–114, doi:10.1007/978-3-319-11936-6_8. short: T. Brázdil, K. Chatterjee, M. Chmelik, V. Forejt, J. Kretinsky, M. Kwiatkowska, D. Parker, M. Ujma, in:, 12th International Symposium on Automated Technology for Verification and Analysis, Springer, 2014, pp. 98–114. conference: end_date: 2014-11-07 location: Sydney, Australia name: 'ATVA: Automated Technology for Verification and Analysis' start_date: 2014-11-03 das_tickbox: '1' date_created: 2018-12-11T11:55:17Z date_published: 2014-11-01T00:00:00Z date_updated: 2026-07-07T13:15:34Z day: '01' department: - _id: KrCh - _id: ToHe doi: 10.1007/978-3-319-11936-6_8 ec_funded: 1 external_id: arxiv: - '1402.2967' fulldoi: https://doi.org/10.1007/978-3-319-11936-6_8 intvolume: ' 8837' language: - iso: eng main_file_link: - open_access: '1' url: http://arxiv.org/abs/1402.2967 month: '11' oa: 1 oa_version: Submitted Version page: 98 - 114 project: - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling - _id: 26241A12-B435-11E9-9278-68D0E5697425 grant_number: '24696' name: Light-regulated ligand traps for spatio-temporal inhibition of cell signaling - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 25F5A88A-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11402-N23 name: Moderne Concurrency Paradigms - _id: 25863FF4-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11407 name: Game Theory - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship publication: 12th International Symposium on Automated Technology for Verification and Analysis publication_status: published publisher: Springer publist_id: '5046' quality_controlled: '1' scopus_import: '1' status: public title: Verification of Markov decision processes using learning algorithms type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 8837 year: '2014' ... --- _id: '2028' abstract: - lang: eng text: 'Understanding the dynamics of noisy neurons remains an important challenge in neuroscience. Here, we describe a simple probabilistic model that accurately describes the firing behavior in a large class (type II) of neurons. To demonstrate the usefulness of this model, we show how it accurately predicts the interspike interval (ISI) distributions, bursting patterns and mean firing rates found by: (1) simulations of the classic Hodgkin-Huxley model with channel noise, (2) experimental data from squid giant axon with a noisy input current and (3) experimental data on noisy firing from a neuron within the suprachiasmatic nucleus (SCN). This simple model has 6 parameters, however, in some cases, two of these parameters are coupled and only 5 parameters account for much of the known behavior. From these parameters, many properties of spiking can be found through simple calculation. Thus, we show how the complex effects of noise can be understood through a simple and general probabilistic model.' acknowledgement: 'This work is supported by AFOSR grant FA 9550-11-1-0165, program grant RPG 24/2012 from the Human Frontiers of Science (DBF) and travel support from the European Commission Marie Curie International Reintegration Grant PIRG04-GA-2008-239429 (KB). DP was supported by NIHR01 GM104987 and the Wyss Institute of Biologically Inspired Engineering. ' article_processing_charge: No author: - first_name: Katarina full_name: Bodova, Katarina id: 2BA24EA0-F248-11E8-B48F-1D18A9856A87 last_name: Bodova orcid: 0000-0002-7214-0171 - first_name: David full_name: Paydarfar, David last_name: Paydarfar - first_name: Daniel full_name: Forger, Daniel last_name: Forger citation: ama: Bodova K, Paydarfar D, Forger D. Characterizing spiking in noisy type II neurons. Journal of Theoretical Biology. 2014;365:40-54. doi:10.1016/j.jtbi.2014.09.041 apa: Bodova, K., Paydarfar, D., & Forger, D. (2014). Characterizing spiking in noisy type II neurons. Journal of Theoretical Biology. Academic Press. https://doi.org/10.1016/j.jtbi.2014.09.041 chicago: Bodova, Katarina, David Paydarfar, and Daniel Forger. “Characterizing Spiking in Noisy Type II Neurons.” Journal of Theoretical Biology. Academic Press, 2014. https://doi.org/10.1016/j.jtbi.2014.09.041. ieee: K. Bodova, D. Paydarfar, and D. Forger, “Characterizing spiking in noisy type II neurons,” Journal of Theoretical Biology, vol. 365. Academic Press, pp. 40–54, 2014. ista: Bodova K, Paydarfar D, Forger D. 2014. Characterizing spiking in noisy type II neurons. Journal of Theoretical Biology. 365, 40–54. mla: Bodova, Katarina, et al. “Characterizing Spiking in Noisy Type II Neurons.” Journal of Theoretical Biology, vol. 365, Academic Press, 2014, pp. 40–54, doi:10.1016/j.jtbi.2014.09.041. short: K. Bodova, D. Paydarfar, D. Forger, Journal of Theoretical Biology 365 (2014) 40–54. corr_author: '1' das_tickbox: '1' date_created: 2018-12-11T11:55:18Z date_published: 2014-10-12T00:00:00Z date_updated: 2026-07-07T13:13:09Z day: '12' ddc: - '570' department: - _id: GaTk doi: 10.1016/j.jtbi.2014.09.041 external_id: isi: - '000347267200005' file: - access_level: open_access checksum: a9dbae18d3233b3dab6944fd3f2cd49e content_type: application/pdf creator: system date_created: 2018-12-12T10:17:58Z date_updated: 2020-07-14T12:45:25Z file_id: '5316' file_name: IST-2016-444-v1+1_1-s2.0-S0022519314005888-main.pdf file_size: 2679222 relation: main_file file_date_updated: 2020-07-14T12:45:25Z fulldoi: https://doi.org/10.1016/j.jtbi.2014.09.041 has_accepted_license: '1' intvolume: ' 365' isi: 1 language: - iso: eng month: '10' oa: 1 oa_version: Published Version page: 40 - 54 publication: Journal of Theoretical Biology publication_status: published publisher: Academic Press publist_id: '5043' pubrep_id: '444' quality_controlled: '1' related_material: link: - relation: erratum url: https://doi.org/10.1016/j.jtbi.2015.03.013 scopus_import: '1' status: public title: Characterizing spiking in noisy type II neurons tmp: image: /images/cc_by_nc_nd.png legal_code_url: https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode name: Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0) short: CC BY-NC-ND (4.0) type: journal_article user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 365 year: '2014' ... --- _id: '5415' abstract: - lang: eng text: 'Recently there has been a significant effort to add quantitative properties in formal verification and synthesis. While weighted automata over finite and infinite words provide a natural and flexible framework to express quantitative properties, perhaps surprisingly, several basic system properties such as average response time cannot be expressed with weighted automata. In this work, we introduce nested weighted automata as a new formalism for expressing important quantitative properties such as average response time. We establish an almost complete decidability picture for the basic decision problems for nested weighted automata, and illustrate its applicability in several domains. ' alternative_title: - IST Austria Technical Report author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Jan full_name: Otop, Jan id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87 last_name: Otop citation: ama: Chatterjee K, Henzinger TA, Otop J. Nested Weighted Automata. IST Austria; 2014. doi:10.15479/AT:IST-2014-170-v1-1 apa: Chatterjee, K., Henzinger, T. A., & Otop, J. (2014). Nested weighted automata. IST Austria. https://doi.org/10.15479/AT:IST-2014-170-v1-1 chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. Nested Weighted Automata. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-170-v1-1. ieee: K. Chatterjee, T. A. Henzinger, and J. Otop, Nested weighted automata. IST Austria, 2014. ista: Chatterjee K, Henzinger TA, Otop J. 2014. Nested weighted automata, IST Austria, 27p. mla: Chatterjee, Krishnendu, et al. Nested Weighted Automata. IST Austria, 2014, doi:10.15479/AT:IST-2014-170-v1-1. short: K. Chatterjee, T.A. Henzinger, J. Otop, Nested Weighted Automata, IST Austria, 2014. date_created: 2018-12-12T11:39:12Z date_published: 2014-02-19T00:00:00Z date_updated: 2026-07-07T14:01:10Z day: '19' ddc: - '004' department: - _id: KrCh - _id: ToHe doi: 10.15479/AT:IST-2014-170-v1-1 file: - access_level: open_access checksum: 31f90dcf2cf899c3f8c6427cfcc2b3c7 content_type: application/pdf creator: system date_created: 2018-12-12T11:53:36Z date_updated: 2020-07-14T12:46:48Z file_id: '5497' file_name: IST-2014-170-v1+1_main.pdf file_size: 573457 relation: main_file file_date_updated: 2020-07-14T12:46:48Z fulldoi: https://doi.org/10.15479/AT:IST-2014-170-v1-1 has_accepted_license: '1' language: - iso: eng month: '02' oa: 1 oa_version: Published Version page: '27' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '170' related_material: record: - id: '5436' relation: later_version status: public - id: '1656' relation: later_version status: public - id: '467' relation: later_version status: public status: public title: Nested weighted automata type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2014' ... --- _id: '2038' abstract: - lang: eng text: Recently, there has been an effort to add quantitative objectives to formal verification and synthesis. We introduce and investigate the extension of temporal logics with quantitative atomic assertions. At the heart of quantitative objectives lies the accumulation of values along a computation. It is often the accumulated sum, as with energy objectives, or the accumulated average, as with mean-payoff objectives. We investigate the extension of temporal logics with the prefix-accumulation assertions Sum(v) ≥ c and Avg(v) ≥ c, where v is a numeric (or Boolean) variable of the system, c is a constant rational number, and Sum(v) and Avg(v) denote the accumulated sum and average of the values of v from the beginning of the computation up to the current point in time. We also allow the path-accumulation assertions LimInfAvg(v) ≥ c and LimSupAvg(v) ≥ c, referring to the average value along an entire infinite computation. We study the border of decidability for such quantitative extensions of various temporal logics. In particular, we show that extending the fragment of CTL that has only the EX, EF, AX, and AG temporal modalities with both prefix-accumulation assertions, or extending LTL with both path-accumulation assertions, results in temporal logics whose model-checking problem is decidable. Moreover, the prefix-accumulation assertions may be generalized with "controlled accumulation," allowing, for example, to specify constraints on the average waiting time between a request and a grant. On the negative side, we show that this branching-time logic is, in a sense, the maximal logic with one or both of the prefix-accumulation assertions that permits a decidable model-checking procedure. Extending a temporal logic that has the EG or EU modalities, such as CTL or LTL, makes the problem undecidable. acknowledgement: The research was supported in part by ERC Starting grant 278410 (QUALITY). article_number: '27' article_processing_charge: No article_type: original author: - first_name: Udi full_name: Boker, Udi id: 31E297B6-F248-11E8-B48F-1D18A9856A87 last_name: Boker - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Orna full_name: Kupferman, Orna last_name: Kupferman citation: ama: Boker U, Chatterjee K, Henzinger TA, Kupferman O. Temporal specifications with accumulative values. ACM Transactions on Computational Logic. 2014;15(4). doi:10.1145/2629686 apa: Boker, U., Chatterjee, K., Henzinger, T. A., & Kupferman, O. (2014). Temporal specifications with accumulative values. ACM Transactions on Computational Logic. ACM. https://doi.org/10.1145/2629686 chicago: Boker, Udi, Krishnendu Chatterjee, Thomas A Henzinger, and Orna Kupferman. “Temporal Specifications with Accumulative Values.” ACM Transactions on Computational Logic. ACM, 2014. https://doi.org/10.1145/2629686. ieee: U. Boker, K. Chatterjee, T. A. Henzinger, and O. Kupferman, “Temporal specifications with accumulative values,” ACM Transactions on Computational Logic, vol. 15, no. 4. ACM, 2014. ista: Boker U, Chatterjee K, Henzinger TA, Kupferman O. 2014. Temporal specifications with accumulative values. ACM Transactions on Computational Logic. 15(4), 27. mla: Boker, Udi, et al. “Temporal Specifications with Accumulative Values.” ACM Transactions on Computational Logic, vol. 15, no. 4, 27, ACM, 2014, doi:10.1145/2629686. short: U. Boker, K. Chatterjee, T.A. Henzinger, O. Kupferman, ACM Transactions on Computational Logic 15 (2014). das_tickbox: '1' date_created: 2018-12-11T11:55:21Z date_published: 2014-09-16T00:00:00Z date_updated: 2026-07-07T14:01:43Z day: '16' ddc: - '000' - '004' department: - _id: ToHe - _id: KrCh doi: 10.1145/2629686 ec_funded: 1 external_id: isi: - '000345570700002' file: - access_level: open_access checksum: 354c41d37500b56320afce94cf9a99c2 content_type: application/pdf creator: system date_created: 2018-12-12T10:10:59Z date_updated: 2020-07-14T12:45:26Z file_id: '4851' file_name: IST-2014-192-v1+1_AccumulativeValues.pdf file_size: 346184 relation: main_file file_date_updated: 2020-07-14T12:45:26Z fulldoi: https://doi.org/10.1145/2629686 has_accepted_license: '1' intvolume: ' 15' isi: 1 issue: '4' language: - iso: eng month: '09' oa: 1 oa_version: Submitted Version project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25F5A88A-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11402-N23 name: Moderne Concurrency Paradigms - _id: 25863FF4-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11407 name: Game Theory - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship publication: ACM Transactions on Computational Logic publication_status: published publisher: ACM publist_id: '5013' pubrep_id: '192' quality_controlled: '1' related_material: record: - id: '5385' relation: earlier_version status: public - id: '3356' relation: earlier_version status: public scopus_import: '1' status: public title: Temporal specifications with accumulative values type: journal_article user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 15 year: '2014' ... --- OA_place: repository OA_type: green _id: '1903' abstract: - lang: eng text: 'We consider two-player zero-sum partial-observation stochastic games on graphs. Based on the information available to the players these games can be classified as follows: (a) general partial-observation (both players have partial view of the game); (b) one-sided partial-observation (one player has partial-observation and the other player has complete-observation); and (c) perfect-observation (both players have complete view of the game). The one-sided partial-observation games subsumes the important special case of one-player partial-observation stochastic games (or partial-observation Markov decision processes (POMDPs)). Based on the randomization available for the strategies, (a) the players may not be allowed to use randomization (pure strategies), or (b) they may choose a probability distribution over actions but the actual random choice is external and not visible to the player (actions invisible), or (c) they may use full randomization. We consider all these classes of games with reachability, and parity objectives that can express all ω-regular objectives. The analysis problems are classified into the qualitative analysis that asks for the existence of a strategy that ensures the objective with probability 1; and the quantitative analysis that asks for the existence of a strategy that ensures the objective with probability at least λ (0,1). In this talk we will cover a wide range of results: for perfect-observation games; for POMDPs; for one-sided partial-observation games; and for general partial-observation games.' alternative_title: - LNCS article_processing_charge: No author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X citation: ama: 'Chatterjee K. Partial-observation stochastic reachability and parity games. In: Vol 8634. Springer; 2014:1-4. doi:10.1007/978-3-662-44522-8_1' apa: 'Chatterjee, K. (2014). Partial-observation stochastic reachability and parity games (Vol. 8634, pp. 1–4). Presented at the MFCS: Mathematical Foundations of Computer Science, Budapest, Hungary: Springer. https://doi.org/10.1007/978-3-662-44522-8_1' chicago: Chatterjee, Krishnendu. “Partial-Observation Stochastic Reachability and Parity Games,” 8634:1–4. Springer, 2014. https://doi.org/10.1007/978-3-662-44522-8_1. ieee: 'K. Chatterjee, “Partial-observation stochastic reachability and parity games,” presented at the MFCS: Mathematical Foundations of Computer Science, Budapest, Hungary, 2014, vol. 8634, no. PART 1, pp. 1–4.' ista: 'Chatterjee K. 2014. Partial-observation stochastic reachability and parity games. MFCS: Mathematical Foundations of Computer Science, LNCS, vol. 8634, 1–4.' mla: Chatterjee, Krishnendu. Partial-Observation Stochastic Reachability and Parity Games. Vol. 8634, no. PART 1, Springer, 2014, pp. 1–4, doi:10.1007/978-3-662-44522-8_1. short: K. Chatterjee, in:, Springer, 2014, pp. 1–4. conference: end_date: 2014-08-29 location: Budapest, Hungary name: 'MFCS: Mathematical Foundations of Computer Science' start_date: 2014-08-25 corr_author: '1' date_created: 2018-12-11T11:54:38Z date_published: 2014-01-01T00:00:00Z date_updated: 2026-07-07T14:01:25Z day: '01' department: - _id: KrCh doi: 10.1007/978-3-662-44522-8_1 ec_funded: 1 fulldoi: https://doi.org/10.1007/978-3-662-44522-8_1 intvolume: ' 8634' issue: PART 1 language: - iso: eng main_file_link: - open_access: '1' url: https://doi.org/10.15479/AT:IST-2011-0007 month: '01' oa: 1 oa_version: Preprint page: 1 - 4 project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25863FF4-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11407 name: Game Theory - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship publication_status: published publisher: Springer publist_id: '5192' pubrep_id: '141' quality_controlled: '1' related_material: record: - id: '5381' relation: earlier_version status: public - id: '2211' relation: later_version status: public scopus_import: '1' status: public title: Partial-observation stochastic reachability and parity games type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 8634 year: '2014' ... --- _id: '2211' abstract: - lang: eng text: 'In two-player finite-state stochastic games of partial observation on graphs, in every state of the graph, the players simultaneously choose an action, and their joint actions determine a probability distribution over the successor states. The game is played for infinitely many rounds and thus the players construct an infinite path in the graph. We consider reachability objectives where the first player tries to ensure a target state to be visited almost-surely (i.e., with probability 1) or positively (i.e., with positive probability), no matter the strategy of the second player. We classify such games according to the information and to the power of randomization available to the players. On the basis of information, the game can be one-sided with either (a) player 1, or (b) player 2 having partial observation (and the other player has perfect observation), or two-sided with (c) both players having partial observation. On the basis of randomization, (a) the players may not be allowed to use randomization (pure strategies), or (b) they may choose a probability distribution over actions but the actual random choice is external and not visible to the player (actions invisible), or (c) they may use full randomization. Our main results for pure strategies are as follows: (1) For one-sided games with player 2 having perfect observation we show that (in contrast to full randomized strategies) belief-based (subset-construction based) strategies are not sufficient, and we present an exponential upper bound on memory both for almost-sure and positive winning strategies; we show that the problem of deciding the existence of almost-sure and positive winning strategies for player 1 is EXPTIME-complete and present symbolic algorithms that avoid the explicit exponential construction. (2) For one-sided games with player 1 having perfect observation we show that nonelementarymemory is both necessary and sufficient for both almost-sure and positive winning strategies. (3) We show that for the general (two-sided) case finite-memory strategies are sufficient for both positive and almost-sure winning, and at least nonelementary memory is required. We establish the equivalence of the almost-sure winning problems for pure strategies and for randomized strategies with actions invisible. Our equivalence result exhibit serious flaws in previous results of the literature: we show a nonelementary memory lower bound for almost-sure winning whereas an exponential upper bound was previously claimed.' article_number: '16' article_processing_charge: No arxiv: 1 author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Laurent full_name: Doyen, Laurent last_name: Doyen citation: ama: 'Chatterjee K, Doyen L. Partial-observation stochastic games: How to win when belief fails. ACM Transactions on Computational Logic. 2014;15(2). doi:10.1145/2579821' apa: 'Chatterjee, K., & Doyen, L. (2014). Partial-observation stochastic games: How to win when belief fails. ACM Transactions on Computational Logic. ACM. https://doi.org/10.1145/2579821' chicago: 'Chatterjee, Krishnendu, and Laurent Doyen. “Partial-Observation Stochastic Games: How to Win When Belief Fails.” ACM Transactions on Computational Logic. ACM, 2014. https://doi.org/10.1145/2579821.' ieee: 'K. Chatterjee and L. Doyen, “Partial-observation stochastic games: How to win when belief fails,” ACM Transactions on Computational Logic, vol. 15, no. 2. ACM, 2014.' ista: 'Chatterjee K, Doyen L. 2014. Partial-observation stochastic games: How to win when belief fails. ACM Transactions on Computational Logic. 15(2), 16.' mla: 'Chatterjee, Krishnendu, and Laurent Doyen. “Partial-Observation Stochastic Games: How to Win When Belief Fails.” ACM Transactions on Computational Logic, vol. 15, no. 2, 16, ACM, 2014, doi:10.1145/2579821.' short: K. Chatterjee, L. Doyen, ACM Transactions on Computational Logic 15 (2014). das_tickbox: '1' date_created: 2018-12-11T11:56:21Z date_published: 2014-04-01T00:00:00Z date_updated: 2026-07-07T14:01:26Z day: '01' department: - _id: KrCh doi: 10.1145/2579821 external_id: arxiv: - '1107.2141' isi: - '000336005000006' fulldoi: https://doi.org/10.1145/2579821 intvolume: ' 15' isi: 1 issue: '2' language: - iso: eng main_file_link: - open_access: '1' url: http://arxiv.org/abs/1107.2141 month: '04' oa: 1 oa_version: Preprint publication: ACM Transactions on Computational Logic publication_status: published publisher: ACM publist_id: '4759' quality_controlled: '1' related_material: record: - id: '5381' relation: earlier_version status: public - id: '1903' relation: earlier_version status: public - id: '2955' relation: earlier_version status: public scopus_import: '1' status: public title: 'Partial-observation stochastic games: How to win when belief fails' type: journal_article user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 15 year: '2014' ... --- _id: '2054' abstract: - lang: eng text: 'We study two-player concurrent games on finite-state graphs played for an infinite number of rounds, where in each round, the two players (player 1 and player 2) choose their moves independently and simultaneously; the current state and the two moves determine the successor state. The objectives are ω-regular winning conditions specified as parity objectives. We consider the qualitative analysis problems: the computation of the almost-sure and limit-sure winning set of states, where player 1 can ensure to win with probability 1 and with probability arbitrarily close to 1, respectively. In general the almost-sure and limit-sure winning strategies require both infinite-memory as well as infinite-precision (to describe probabilities). While the qualitative analysis problem for concurrent parity games with infinite-memory, infinite-precision randomized strategies was studied before, we study the bounded-rationality problem for qualitative analysis of concurrent parity games, where the strategy set for player 1 is restricted to bounded-resource strategies. In terms of precision, strategies can be deterministic, uniform, finite-precision, or infinite-precision; and in terms of memory, strategies can be memoryless, finite-memory, or infinite-memory. We present a precise and complete characterization of the qualitative winning sets for all combinations of classes of strategies. In particular, we show that uniform memoryless strategies are as powerful as finite-precision infinite-memory strategies, and infinite-precision memoryless strategies are as powerful as infinite-precision finite-memory strategies. We show that the winning sets can be computed in (n2d+3) time, where n is the size of the game structure and 2d is the number of priorities (or colors), and our algorithms are symbolic. The membership problem of whether a state belongs to a winning set can be decided in NP ∩ coNP. Our symbolic algorithms are based on a characterization of the winning sets as μ-calculus formulas, however, our μ-calculus formulas are crucially different from the ones for concurrent parity games (without bounded rationality); and our memoryless witness strategy constructions are significantly different from the infinite-memory witness strategy constructions for concurrent parity games.' alternative_title: - LNCS author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X citation: ama: 'Chatterjee K. Qualitative concurrent parity games: Bounded rationality. In: Baldan P, Gorla D, eds. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol 8704. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2014:544-559. doi:10.1007/978-3-662-44584-6_37' apa: 'Chatterjee, K. (2014). Qualitative concurrent parity games: Bounded rationality. In P. Baldan & D. Gorla (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8704, pp. 544–559). Rome, Italy: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.1007/978-3-662-44584-6_37' chicago: 'Chatterjee, Krishnendu. “Qualitative Concurrent Parity Games: Bounded Rationality.” In Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), edited by Paolo Baldan and Daniele Gorla, 8704:544–59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014. https://doi.org/10.1007/978-3-662-44584-6_37.' ieee: 'K. Chatterjee, “Qualitative concurrent parity games: Bounded rationality,” in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Rome, Italy, 2014, vol. 8704, pp. 544–559.' ista: 'Chatterjee K. 2014. Qualitative concurrent parity games: Bounded rationality. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). CONCUR: Concurrency Theory, LNCS, vol. 8704, 544–559.' mla: 'Chatterjee, Krishnendu. “Qualitative Concurrent Parity Games: Bounded Rationality.” Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), edited by Paolo Baldan and Daniele Gorla, vol. 8704, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014, pp. 544–59, doi:10.1007/978-3-662-44584-6_37.' short: K. Chatterjee, in:, P. Baldan, D. Gorla (Eds.), Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014, pp. 544–559. conference: end_date: 2014-09-05 location: Rome, Italy name: 'CONCUR: Concurrency Theory' start_date: 2014-09-02 corr_author: '1' date_created: 2018-12-11T11:55:27Z date_published: 2014-09-01T00:00:00Z date_updated: 2026-07-07T14:02:37Z day: '01' department: - _id: KrCh doi: 10.1007/978-3-662-44584-6_37 ec_funded: 1 editor: - first_name: Paolo full_name: Baldan, Paolo last_name: Baldan - first_name: Daniele full_name: Gorla, Daniele last_name: Gorla fulldoi: https://doi.org/10.1007/978-3-662-44584-6_37 intvolume: ' 8704' language: - iso: eng month: '09' oa_version: None page: 544 - 559 project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25863FF4-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11407 name: Game Theory - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship publication: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) publication_status: published publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik publist_id: '4992' quality_controlled: '1' related_material: record: - id: '3354' relation: earlier_version status: public scopus_import: '1' status: public title: 'Qualitative concurrent parity games: Bounded rationality' type: conference user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87 volume: 8704 year: '2014' ... --- _id: '535' abstract: - lang: eng text: Energy games belong to a class of turn-based two-player infinite-duration games played on a weighted directed graph. It is one of the rare and intriguing combinatorial problems that lie in NP∩co-NP, but are not known to be in P. The existence of polynomial-time algorithms has been a major open problem for decades and apart from pseudopolynomial algorithms there is no algorithm that solves any non-trivial subclass in polynomial time. In this paper, we give several results based on the weight structures of the graph. First, we identify a notion of penalty and present a polynomial-time algorithm when the penalty is large. Our algorithm is the first polynomial-time algorithm on a large class of weighted graphs. It includes several worst-case instances on which previous algorithms, such as value iteration and random facet algorithms, require at least sub-exponential time. Our main technique is developing the first non-trivial approximation algorithm and showing how to convert it to an exact algorithm. Moreover, we show that in a practical case in verification where weights are clustered around a constant number of values, the energy game problem can be solved in polynomial time. We also show that the problem is still as hard as in general when the clique-width is bounded or the graph is strongly ergodic, suggesting that restricting the graph structure does not necessarily help. article_processing_charge: No article_type: original arxiv: 1 author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Monika H full_name: Henzinger, Monika H id: 540c9bbd-f2de-11ec-812d-d04a5be85630 last_name: Henzinger orcid: 0000-0002-5008-6530 - first_name: Sebastian full_name: Krinninger, Sebastian last_name: Krinninger - first_name: Danupon full_name: Nanongkai, Danupon last_name: Nanongkai citation: ama: Chatterjee K, Henzinger M, Krinninger S, Nanongkai D. Polynomial-time algorithms for energy games with special weight structures. Algorithmica. 2014;70(3):457-492. doi:10.1007/s00453-013-9843-7 apa: Chatterjee, K., Henzinger, M., Krinninger, S., & Nanongkai, D. (2014). Polynomial-time algorithms for energy games with special weight structures. Algorithmica. Springer. https://doi.org/10.1007/s00453-013-9843-7 chicago: Chatterjee, Krishnendu, Monika Henzinger, Sebastian Krinninger, and Danupon Nanongkai. “Polynomial-Time Algorithms for Energy Games with Special Weight Structures.” Algorithmica. Springer, 2014. https://doi.org/10.1007/s00453-013-9843-7. ieee: K. Chatterjee, M. Henzinger, S. Krinninger, and D. Nanongkai, “Polynomial-time algorithms for energy games with special weight structures,” Algorithmica, vol. 70, no. 3. Springer, pp. 457–492, 2014. ista: Chatterjee K, Henzinger M, Krinninger S, Nanongkai D. 2014. Polynomial-time algorithms for energy games with special weight structures. Algorithmica. 70(3), 457–492. mla: Chatterjee, Krishnendu, et al. “Polynomial-Time Algorithms for Energy Games with Special Weight Structures.” Algorithmica, vol. 70, no. 3, Springer, 2014, pp. 457–92, doi:10.1007/s00453-013-9843-7. short: K. Chatterjee, M. Henzinger, S. Krinninger, D. Nanongkai, Algorithmica 70 (2014) 457–492. date_created: 2018-12-11T11:47:01Z date_published: 2014-11-01T00:00:00Z date_updated: 2026-07-08T05:50:38Z day: '01' department: - _id: KrCh doi: 10.1007/s00453-013-9843-7 ec_funded: 1 external_id: arxiv: - '1604.08234' isi: - '000340552300005' fulldoi: https://doi.org/10.1007/s00453-013-9843-7 intvolume: ' 70' isi: 1 issue: '3' language: - iso: eng main_file_link: - open_access: '1' url: https://arxiv.org/abs/1604.08234 month: '11' oa: 1 oa_version: Preprint page: 457 - 492 project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25863FF4-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11407 name: Game Theory - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship publication: Algorithmica publication_status: published publisher: Springer publist_id: '7282' quality_controlled: '1' related_material: record: - id: '10905' relation: earlier_version status: public scopus_import: '1' status: public title: Polynomial-time algorithms for energy games with special weight structures type: journal_article user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345 volume: 70 year: '2014' ... --- _id: '1872' abstract: - lang: eng text: Extensionality axioms are common when reasoning about data collections, such as arrays and functions in program analysis, or sets in mathematics. An extensionality axiom asserts that two collections are equal if they consist of the same elements at the same indices. Using extensionality is often required to show that two collections are equal. A typical example is the set theory theorem (∀x)(∀y)x∪y = y ∪x. Interestingly, while humans have no problem with proving such set identities using extensionality, they are very hard for superposition theorem provers because of the calculi they use. In this paper we show how addition of a new inference rule, called extensionality resolution, allows first-order theorem provers to easily solve problems no modern first-order theorem prover can solve. We illustrate this by running the VAMPIRE theorem prover with extensionality resolution on a number of set theory and array problems. Extensionality resolution helps VAMPIRE to solve problems from the TPTP library of first-order problems that were never solved before by any prover. acknowledgement: This research was supported in part by the Austrian National Research Network RiSE (S11410-N23). alternative_title: - LNCS article_processing_charge: No author: - first_name: Ashutosh full_name: Gupta, Ashutosh id: 335E5684-F248-11E8-B48F-1D18A9856A87 last_name: Gupta - first_name: Laura full_name: Kovács, Laura last_name: Kovács - first_name: Bernhard full_name: Kragl, Bernhard id: 320FC952-F248-11E8-B48F-1D18A9856A87 last_name: Kragl orcid: 0000-0001-7745-9117 - first_name: Andrei full_name: Voronkov, Andrei last_name: Voronkov citation: ama: 'Gupta A, Kovács L, Kragl B, Voronkov A. Extensional crisis and proving identity. In: 12th International Symposium on Automated Technology for Verification and Analysis. Vol 8837. Springer; 2014:185-200. doi:10.1007/978-3-319-11936-6_14' apa: 'Gupta, A., Kovács, L., Kragl, B., & Voronkov, A. (2014). Extensional crisis and proving identity. In 12th International Symposium on Automated Technology for Verification and Analysis (Vol. 8837, pp. 185–200). Sydney, Australia: Springer. https://doi.org/10.1007/978-3-319-11936-6_14' chicago: Gupta, Ashutosh, Laura Kovács, Bernhard Kragl, and Andrei Voronkov. “Extensional Crisis and Proving Identity.” In 12th International Symposium on Automated Technology for Verification and Analysis, 8837:185–200. Springer, 2014. https://doi.org/10.1007/978-3-319-11936-6_14. ieee: A. Gupta, L. Kovács, B. Kragl, and A. Voronkov, “Extensional crisis and proving identity,” in 12th International Symposium on Automated Technology for Verification and Analysis, Sydney, Australia, 2014, vol. 8837, pp. 185–200. ista: 'Gupta A, Kovács L, Kragl B, Voronkov A. 2014. Extensional crisis and proving identity. 12th International Symposium on Automated Technology for Verification and Analysis. ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 8837, 185–200.' mla: Gupta, Ashutosh, et al. “Extensional Crisis and Proving Identity.” 12th International Symposium on Automated Technology for Verification and Analysis, vol. 8837, Springer, 2014, pp. 185–200, doi:10.1007/978-3-319-11936-6_14. short: A. Gupta, L. Kovács, B. Kragl, A. Voronkov, in:, 12th International Symposium on Automated Technology for Verification and Analysis, Springer, 2014, pp. 185–200. conference: end_date: 2014-11-07 location: Sydney, Australia name: 'ATVA: Automated Technology for Verification and Analysis' start_date: 2014-11-03 das_tickbox: '1' date_created: 2018-12-11T11:54:28Z date_published: 2014-01-01T00:00:00Z date_updated: 2026-07-08T06:49:33Z day: '01' ddc: - '000' department: - _id: ToHe doi: 10.1007/978-3-319-11936-6_14 ec_funded: 1 file: - access_level: open_access checksum: af4bd3fc1f4c93075e4dc5cbf625fe7b content_type: application/pdf creator: system date_created: 2018-12-12T10:10:15Z date_updated: 2020-07-14T12:45:19Z file_id: '4801' file_name: IST-2016-641-v1+1_atva2014.pdf file_size: 244294 relation: main_file file_date_updated: 2020-07-14T12:45:19Z fulldoi: https://doi.org/10.1007/978-3-319-11936-6_14 has_accepted_license: '1' intvolume: ' 8837' language: - iso: eng month: '01' oa: 1 oa_version: Submitted Version page: 185 - 200 project: - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling - _id: 25F5A88A-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11402-N23 name: Moderne Concurrency Paradigms publication: 12th International Symposium on Automated Technology for Verification and Analysis publication_status: published publisher: Springer publist_id: '5226' pubrep_id: '641' quality_controlled: '1' scopus_import: '1' status: public title: Extensional crisis and proving identity type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 8837 year: '2014' ... --- _id: '9753' abstract: - lang: eng text: 'Background: The brood of ants and other social insects is highly susceptible to pathogens, particularly those that penetrate the soft larval and pupal cuticle. We here test whether the presence of a pupal cocoon, which occurs in some ant species but not in others, affects the sanitary brood care and fungal infection patterns after exposure to the entomopathogenic fungus Metarhizium brunneum. We use a) a comparative approach analysing four species with either naked or cocooned pupae and b) a within-species analysis of a single ant species, in which both pupal types co-exist in the same colony. Results: We found that the presence of a cocoon did not compromise fungal pathogen detection by the ants and that species with cocooned pupae increased brood grooming after pathogen exposure. All tested ant species further removed brood from their nests, which was predominantly expressed towards larvae and naked pupae treated with the live fungal pathogen. In contrast, cocooned pupae exposed to live fungus were not removed at higher rates than cocooned pupae exposed to dead fungus or a sham control. Consistent with this, exposure to the live fungus caused high numbers of infections and fungal outgrowth in larvae and naked pupae, but not in cocooned pupae. Moreover, the ants consistently removed the brood prior to fungal outgrowth, ensuring a clean brood chamber. Conclusion: Our study suggests that the pupal cocoon has a protective effect against fungal infection, causing an adaptive change in sanitary behaviours by the ants. It further demonstrates that brood removal - originally described for honeybees as “hygienic behaviour” – is a widespread sanitary behaviour in ants, which likely has important implications on disease dynamics in social insect colonies.' article_processing_charge: No author: - first_name: Simon full_name: Tragust, Simon id: 35A7A418-F248-11E8-B48F-1D18A9856A87 last_name: Tragust - first_name: Line V full_name: Ugelvig, Line V id: 3DC97C8E-F248-11E8-B48F-1D18A9856A87 last_name: Ugelvig orcid: 0000-0003-1832-8883 - first_name: Michel full_name: Chapuisat, Michel last_name: Chapuisat - first_name: Jürgen full_name: Heinze, Jürgen last_name: Heinze - first_name: Sylvia full_name: Cremer, Sylvia id: 2F64EC8C-F248-11E8-B48F-1D18A9856A87 last_name: Cremer orcid: 0000-0002-2193-3868 citation: ama: 'Tragust S, Ugelvig LV, Chapuisat M, Heinze J, Cremer S. Data from: Pupal cocoons affect sanitary brood care and limit fungal infections in ant colonies. 2014. doi:10.5061/dryad.nc0gc' apa: 'Tragust, S., Ugelvig, L. V., Chapuisat, M., Heinze, J., & Cremer, S. (2014). Data from: Pupal cocoons affect sanitary brood care and limit fungal infections in ant colonies. Dryad. https://doi.org/10.5061/dryad.nc0gc' chicago: 'Tragust, Simon, Line V Ugelvig, Michel Chapuisat, Jürgen Heinze, and Sylvia Cremer. “Data from: Pupal Cocoons Affect Sanitary Brood Care and Limit Fungal Infections in Ant Colonies.” Dryad, 2014. https://doi.org/10.5061/dryad.nc0gc.' ieee: 'S. Tragust, L. V. Ugelvig, M. Chapuisat, J. Heinze, and S. Cremer, “Data from: Pupal cocoons affect sanitary brood care and limit fungal infections in ant colonies.” Dryad, 2014.' ista: 'Tragust S, Ugelvig LV, Chapuisat M, Heinze J, Cremer S. 2014. Data from: Pupal cocoons affect sanitary brood care and limit fungal infections in ant colonies, Dryad, 10.5061/dryad.nc0gc.' mla: 'Tragust, Simon, et al. Data from: Pupal Cocoons Affect Sanitary Brood Care and Limit Fungal Infections in Ant Colonies. Dryad, 2014, doi:10.5061/dryad.nc0gc.' short: S. Tragust, L.V. Ugelvig, M. Chapuisat, J. Heinze, S. Cremer, (2014). date_created: 2021-07-30T08:24:11Z date_published: 2014-10-08T00:00:00Z date_updated: 2026-07-28T09:35:11Z day: '08' department: - _id: SyCr doi: 10.5061/dryad.nc0gc fulldoi: https://doi.org/10.5061/dryad.nc0gc main_file_link: - open_access: '1' url: https://doi.org/10.5061/dryad.nc0gc month: '10' oa: 1 oa_version: Published Version publisher: Dryad related_material: record: - id: '2284' relation: used_in_publication status: public status: public title: 'Data from: Pupal cocoons affect sanitary brood care and limit fungal infections in ant colonies' type: research_data_reference user_id: 6785fbc1-c503-11eb-8a32-93094b40e1cf year: '2014' ... --- _id: '2250' abstract: - lang: eng text: The genome sequences of new viruses often contain many "orphan" or "taxon-specific" proteins apparently lacking homologs. However, because viral proteins evolve very fast, commonly used sequence similarity detection methods such as BLAST may overlook homologs. We analyzed a data set of proteins from RNA viruses characterized as "genus specific" by BLAST. More powerful methods developed recently, such as HHblits or HHpred (available through web-based, user-friendly interfaces), could detect distant homologs of a quarter of these proteins, suggesting that these methods should be used to annotate viral genomes. In-depth manual analyses of a subset of the remaining sequences, guided by contextual information such as taxonomy, gene order, or domain cooccurrence, identified distant homologs of another third. Thus, a combination of powerful automated methods and manual analyses can uncover distant homologs of many proteins thought to be orphans. We expect these methodological results to be also applicable to cellular organisms, since they generally evolve much more slowly than RNA viruses. As an application, we reanalyzed the genome of a bee pathogen, Chronic bee paralysis virus (CBPV). We could identify homologs of most of its proteins thought to be orphans; in each case, identifying homologs provided functional clues. We discovered that CBPV encodes a domain homologous to the Alphavirus methyltransferase-guanylyltransferase; a putative membrane protein, SP24, with homologs in unrelated insect viruses and insect-transmitted plant viruses having different morphologies (cileviruses, higreviruses, blunerviruses, negeviruses); and a putative virion glycoprotein, ORF2, also found in negeviruses. SP24 and ORF2 are probably major structural components of the virionsd. article_processing_charge: No author: - first_name: Durga full_name: Kuchibhatla, Durga last_name: Kuchibhatla - first_name: Westley full_name: Sherman, Westley last_name: Sherman - first_name: Betty full_name: Chung, Betty last_name: Chung - first_name: Shelley full_name: Cook, Shelley last_name: Cook - first_name: Georg full_name: Schneider, Georg id: 329095A0-F248-11E8-B48F-1D18A9856A87 last_name: Schneider - first_name: Birgit full_name: Eisenhaber, Birgit last_name: Eisenhaber - first_name: David full_name: Karlin, David last_name: Karlin citation: ama: Kuchibhatla D, Sherman W, Chung B, et al. Powerful sequence similarity search methods and in-depth manual analyses can identify remote homologs in many apparently “orphan” viral proteins. Journal of Virology. 2014;88(1):10-20. doi:10.1128/JVI.02595-13 apa: Kuchibhatla, D., Sherman, W., Chung, B., Cook, S., Schneider, G., Eisenhaber, B., & Karlin, D. (2014). Powerful sequence similarity search methods and in-depth manual analyses can identify remote homologs in many apparently “orphan” viral proteins. Journal of Virology. ASM. https://doi.org/10.1128/JVI.02595-13 chicago: Kuchibhatla, Durga, Westley Sherman, Betty Chung, Shelley Cook, Georg Schneider, Birgit Eisenhaber, and David Karlin. “Powerful Sequence Similarity Search Methods and In-Depth Manual Analyses Can Identify Remote Homologs in Many Apparently ‘Orphan’ Viral Proteins.” Journal of Virology. ASM, 2014. https://doi.org/10.1128/JVI.02595-13. ieee: D. Kuchibhatla et al., “Powerful sequence similarity search methods and in-depth manual analyses can identify remote homologs in many apparently ‘orphan’ viral proteins,” Journal of Virology, vol. 88, no. 1. ASM, pp. 10–20, 2014. ista: Kuchibhatla D, Sherman W, Chung B, Cook S, Schneider G, Eisenhaber B, Karlin D. 2014. Powerful sequence similarity search methods and in-depth manual analyses can identify remote homologs in many apparently ‘orphan’ viral proteins. Journal of Virology. 88(1), 10–20. mla: Kuchibhatla, Durga, et al. “Powerful Sequence Similarity Search Methods and In-Depth Manual Analyses Can Identify Remote Homologs in Many Apparently ‘Orphan’ Viral Proteins.” Journal of Virology, vol. 88, no. 1, ASM, 2014, pp. 10–20, doi:10.1128/JVI.02595-13. short: D. Kuchibhatla, W. Sherman, B. Chung, S. Cook, G. Schneider, B. Eisenhaber, D. Karlin, Journal of Virology 88 (2014) 10–20. das_tickbox: '1' date_created: 2018-12-11T11:56:34Z date_published: 2014-01-01T00:00:00Z date_updated: 2026-07-28T10:18:04Z day: '01' ddc: - '570' department: - _id: MD doi: 10.1128/JVI.02595-13 external_id: isi: - '000329194600002' file: - access_level: open_access checksum: 2c121b5e884992dfec5605bdf4e659da content_type: application/pdf creator: system date_created: 2018-12-12T10:13:43Z date_updated: 2020-07-14T12:45:34Z file_id: '5029' file_name: IST-2016-417-v1+1_J._Virol.-2014-Kuchibhatla-10-20.pdf file_size: 825756 relation: main_file file_date_updated: 2020-07-14T12:45:34Z fulldoi: https://doi.org/10.1128/JVI.02595-13 has_accepted_license: '1' intvolume: ' 88' isi: 1 issue: '1' language: - iso: eng license: https://creativecommons.org/licenses/by/3.0/ month: '01' oa: 1 oa_version: Published Version page: 10 - 20 publication: Journal of Virology publication_identifier: issn: - 0022-538X publication_status: published publisher: ASM publist_id: '4698' pubrep_id: '417' quality_controlled: '1' scopus_import: '1' status: public title: Powerful sequence similarity search methods and in-depth manual analyses can identify remote homologs in many apparently "orphan" viral proteins tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/3.0/legalcode name: Creative Commons Attribution 3.0 Unported (CC BY 3.0) short: CC BY (3.0) type: journal_article user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 88 year: '2014' ... --- _id: '2716' abstract: - lang: eng text: Multi-dimensional mean-payoff and energy games provide the mathematical foundation for the quantitative study of reactive systems, and play a central role in the emerging quantitative theory of verification and synthesis. In this work, we study the strategy synthesis problem for games with such multi-dimensional objectives along with a parity condition, a canonical way to express ω ω -regular conditions. While in general, the winning strategies in such games may require infinite memory, for synthesis the most relevant problem is the construction of a finite-memory winning strategy (if one exists). Our main contributions are as follows. First, we show a tight exponential bound (matching upper and lower bounds) on the memory required for finite-memory winning strategies in both multi-dimensional mean-payoff and energy games along with parity objectives. This significantly improves the triple exponential upper bound for multi energy games (without parity) that could be derived from results in literature for games on vector addition systems with states. Second, we present an optimal symbolic and incremental algorithm to compute a finite-memory winning strategy (if one exists) in such games. Finally, we give a complete characterization of when finite memory of strategies can be traded off for randomness. In particular, we show that for one-dimension mean-payoff parity games, randomized memoryless strategies are as powerful as their pure finite-memory counterparts. acknowledgement: "Krishnendu Chatterjee is supported by Austrian Science Fund (FWF) Grant No P 23499-N23, FWF NFN Grant No S11407 (RiSE), ERC Starting Grant (279307: Graph Games) and Microsoft faculty fellowship. Mickael Randour is supported by F.R.S.-FNRS. fellowship. \r\nJean-François Raskin is supported by ERC Starting Grant (279499: inVEST).Thanks to D. Sbabo for useful pointers, V. Bruyère for comments on a preliminary draft, and A. Bohy for fruitful discussions about the Acacia+ tool. We are grateful to the anonymous reviewers for their insightful comments. " article_processing_charge: No article_type: original arxiv: 1 author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Mickael full_name: Randour, Mickael last_name: Randour - first_name: Jean full_name: Raskin, Jean last_name: Raskin citation: ama: Chatterjee K, Randour M, Raskin J. Strategy synthesis for multi-dimensional quantitative objectives. Acta Informatica. 2014;51(3-4):129-163. doi:10.1007/s00236-013-0182-6 apa: Chatterjee, K., Randour, M., & Raskin, J. (2014). Strategy synthesis for multi-dimensional quantitative objectives. Acta Informatica. Springer. https://doi.org/10.1007/s00236-013-0182-6 chicago: Chatterjee, Krishnendu, Mickael Randour, and Jean Raskin. “Strategy Synthesis for Multi-Dimensional Quantitative Objectives.” Acta Informatica. Springer, 2014. https://doi.org/10.1007/s00236-013-0182-6. ieee: K. Chatterjee, M. Randour, and J. Raskin, “Strategy synthesis for multi-dimensional quantitative objectives,” Acta Informatica, vol. 51, no. 3–4. Springer, pp. 129–163, 2014. ista: Chatterjee K, Randour M, Raskin J. 2014. Strategy synthesis for multi-dimensional quantitative objectives. Acta Informatica. 51(3–4), 129–163. mla: Chatterjee, Krishnendu, et al. “Strategy Synthesis for Multi-Dimensional Quantitative Objectives.” Acta Informatica, vol. 51, no. 3–4, Springer, 2014, pp. 129–63, doi:10.1007/s00236-013-0182-6. short: K. Chatterjee, M. Randour, J. Raskin, Acta Informatica 51 (2014) 129–163. das_tickbox: '1' date_created: 2018-12-11T11:59:14Z date_published: 2014-06-01T00:00:00Z date_updated: 2026-07-28T11:24:52Z day: '01' department: - _id: KrCh doi: 10.1007/s00236-013-0182-6 ec_funded: 1 external_id: arxiv: - '1201.5073' isi: - '000335981500002' fulldoi: https://doi.org/10.1007/s00236-013-0182-6 intvolume: ' 51' isi: 1 issue: 3-4 language: - iso: eng main_file_link: - open_access: '1' url: http://arxiv.org/abs/1201.5073 month: '06' oa: 1 oa_version: Preprint page: 129 - 163 project: - _id: 25863FF4-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11407 name: Game Theory - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship publication: Acta Informatica publication_status: published publisher: Springer publist_id: '4176' quality_controlled: '1' related_material: record: - id: '10904' relation: earlier_version status: public scopus_import: '1' status: public title: Strategy synthesis for multi-dimensional quantitative objectives type: journal_article user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 51 year: '2014' ... --- _id: '254' abstract: - lang: eng text: A new "polynomial sieve" is presented and used to show that almost all integers have at most one representation as a sum of two values of a given polynomial of degree at least 3. acknowledgement: While working on this paper, the author was supported by ERC grant 306457 and a Philip Leverhulme Prize. article_processing_charge: No author: - first_name: Timothy D full_name: Browning, Timothy D id: 35827D50-F248-11E8-B48F-1D18A9856A87 last_name: Browning orcid: 0000-0002-8314-0177 citation: ama: Browning TD. The polynomial sieve and equal sums of like polynomials. International Mathematics Research Notices. 2014;2015(7):1987-2019. doi:10.1093/imrn/rnt350 apa: Browning, T. D. (2014). The polynomial sieve and equal sums of like polynomials. International Mathematics Research Notices. Oxford University Press. https://doi.org/10.1093/imrn/rnt350 chicago: Browning, Timothy D. “The Polynomial Sieve and Equal Sums of like Polynomials.” International Mathematics Research Notices. Oxford University Press, 2014. https://doi.org/10.1093/imrn/rnt350. ieee: T. D. Browning, “The polynomial sieve and equal sums of like polynomials,” International Mathematics Research Notices, vol. 2015, no. 7. Oxford University Press, pp. 1987–2019, 2014. ista: Browning TD. 2014. The polynomial sieve and equal sums of like polynomials. International Mathematics Research Notices. 2015(7), 1987–2019. mla: Browning, Timothy D. “The Polynomial Sieve and Equal Sums of like Polynomials.” International Mathematics Research Notices, vol. 2015, no. 7, Oxford University Press, 2014, pp. 1987–2019, doi:10.1093/imrn/rnt350. short: T.D. Browning, International Mathematics Research Notices 2015 (2014) 1987–2019. date_created: 2018-12-11T11:45:27Z date_published: 2014-01-31T00:00:00Z date_updated: 2026-07-29T09:59:56Z day: '31' doi: 10.1093/imrn/rnt350 extern: '1' fulldoi: https://doi.org/10.1093/imrn/rnt350 intvolume: ' 2015' issue: '7' language: - iso: eng month: '01' oa_version: None page: 1987 - 2019 publication: International Mathematics Research Notices publication_status: published publisher: Oxford University Press publist_id: '7648' quality_controlled: '1' related_material: link: - relation: erratum url: https://doi.org/10.1093/imrn/rnae066 record: - id: '19051' relation: later_version status: public scopus_import: '1' status: public title: The polynomial sieve and equal sums of like polynomials type: journal_article user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 2015 year: '2014' ... --- OA_place: publisher _id: '1395' abstract: - lang: eng text: In this thesis I studied various individual and social immune defences employed by the invasive garden ant Lasius neglectus mostly against entomopathogenic fungi. The first two chapters of this thesis address the phenomenon of 'social immunisation'. Social immunisation, that is the immunological protection of group members due to social contact to a pathogen-exposed nestmate, has been described in various social insect species against different types of pathogens. However, in the case of entomopathogenic fungi it has, so far, only been demonstrated that social immunisation exists at all. Its underlying mechanisms r any other properties were, however, unknown. In the first chapter of this thesis I identified the mechanistic basis of social immunisation in L. neglectus against the entomopathogenous fungus Metarhizium. I could show that nestmates of a pathogen-exposed individual contract low-level infections due to social interactions. These low-level infections are, however, non-lethal and cause an active stimulation of the immune system, which protects the nestmates upon subsequent pathogen encounters. In the second chapter of this thesis I investigated the specificity and colony level effects of social immunisation. I demonstrated that the protection conferred by social immunisation is highly specific, protecting ants only against the same pathogen strain. In addition, depending on the respective context, social immunisation may even cause fitness costs. I further showed that social immunisation crucially affects sanitary behaviour and disease dynamics within ant groups. In the third chapter of this thesis I studied the effects of the ectosymbiotic fungus Laboulbenia formicarum on its host L. neglectus. Although Laboulbeniales are the largest order of insect-parasitic fungi, research concerning host fitness consequence is sparse. I showed that highly Laboulbenia-infected ants sustain fitness costs under resource limitation, however, gain fitness benefits when exposed to an entomopathogenus fungus. These effects are probably cause by a prophylactic upregulation of behavioural as well as physiological immune defences in highly infected ants. alternative_title: - ISTA Thesis article_processing_charge: No author: - first_name: Matthias full_name: Konrad, Matthias id: 46528076-F248-11E8-B48F-1D18A9856A87 last_name: Konrad citation: ama: 'Konrad M. Immune defences in ants: Effects of social immunisation and a fungal ectosymbiont in the ant Lasius neglectus. 2014.' apa: 'Konrad, M. (2014). Immune defences in ants: Effects of social immunisation and a fungal ectosymbiont in the ant Lasius neglectus. Institute of Science and Technology Austria.' chicago: 'Konrad, Matthias. “Immune Defences in Ants: Effects of Social Immunisation and a Fungal Ectosymbiont in the Ant Lasius Neglectus.” Institute of Science and Technology Austria, 2014.' ieee: 'M. Konrad, “Immune defences in ants: Effects of social immunisation and a fungal ectosymbiont in the ant Lasius neglectus,” Institute of Science and Technology Austria, 2014.' ista: 'Konrad M. 2014. Immune defences in ants: Effects of social immunisation and a fungal ectosymbiont in the ant Lasius neglectus. Institute of Science and Technology Austria.' mla: 'Konrad, Matthias. Immune Defences in Ants: Effects of Social Immunisation and a Fungal Ectosymbiont in the Ant Lasius Neglectus. Institute of Science and Technology Austria, 2014.' short: 'M. Konrad, Immune Defences in Ants: Effects of Social Immunisation and a Fungal Ectosymbiont in the Ant Lasius Neglectus, Institute of Science and Technology Austria, 2014.' corr_author: '1' date_created: 2018-12-11T11:51:46Z date_published: 2014-02-01T00:00:00Z date_updated: 2026-07-29T10:01:24Z day: '01' degree_awarded: PhD department: - _id: SyCr - _id: GradSch doi_confirm: '1' language: - iso: eng month: '02' oa_version: None page: '131' publication_identifier: issn: - 2663-337X publication_status: published publisher: Institute of Science and Technology Austria publist_id: '5814' status: public supervisor: - first_name: Sylvia M full_name: Cremer, Sylvia M id: 2F64EC8C-F248-11E8-B48F-1D18A9856A87 last_name: Cremer orcid: 0000-0002-2193-3868 title: 'Immune defences in ants: Effects of social immunisation and a fungal ectosymbiont in the ant Lasius neglectus' type: dissertation user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9 year: '2014' ... --- OA_place: publisher _id: '1404' abstract: - lang: eng text: "The co-evolution of hosts and pathogens is characterized by continuous adaptations of both parties. Pathogens of social insects need to adapt towards disease defences at two levels: 1) individual immunity of each colony member consisting of behavioural defence strategies as well as humoral and cellular immune responses and 2) social immunity that is collectively performed by all group members comprising behavioural, physiological and organisational defence strategies.\r\n\r\nTo disentangle the selection pressure on pathogens by the collective versus individual level of disease defence in social insects, we performed an evolution experiment using the Argentine Ant, Linepithema humile, as a host and a mixture of the general insect pathogenic fungus Metarhizium spp. (6 strains) as a pathogen. We allowed pathogen evolution over 10 serial host passages to two different evolution host treatments: (1) only individual host immunity in a single host treatment, and (2) simultaneously acting individual and social immunity in a social host treatment, in which an exposed ant was accompanied by two untreated nestmates.\r\n\r\nBefore starting the pathogen evolution experiment, the 6 Metarhizium spp. strains were characterised concerning conidiospore size killing rates in singly and socially reared ants, their competitiveness under coinfecting conditions and their influence on ant behaviour. We analysed how the ancestral atrain mixture changed in conidiospere size, killing rate and strain composition dependent on host treatment (single or social hosts) during 10 passages and found that killing rate and conidiospere size of the pathogen increased under both evolution regimes, but different depending on host treatment.\r\n\r\nTesting the evolved strain mixtures that evolved under either the single or social host treatment under both single and social current rearing conditions in a full factorial design experiment revealed that the additional collective defences in insect societies add new selection pressure for their coevolving pathogens that compromise their ability to adapt to its host at the group level. To our knowledge, this is the first study directly measuring the influence of social immunity on pathogen evolution." acknowledgement: This work was funded by the DFG and the ERC. alternative_title: - ISTA Thesis article_processing_charge: No author: - first_name: Miriam full_name: Stock, Miriam id: 42462816-F248-11E8-B48F-1D18A9856A87 last_name: Stock citation: ama: Stock M. Evolution of a fungal pathogen towards individual versus social immunity in ants. 2014. apa: Stock, M. (2014). Evolution of a fungal pathogen towards individual versus social immunity in ants. Institute of Science and Technology Austria. chicago: Stock, Miriam. “Evolution of a Fungal Pathogen towards Individual versus Social Immunity in Ants.” Institute of Science and Technology Austria, 2014. ieee: M. Stock, “Evolution of a fungal pathogen towards individual versus social immunity in ants,” Institute of Science and Technology Austria, 2014. ista: Stock M. 2014. Evolution of a fungal pathogen towards individual versus social immunity in ants. Institute of Science and Technology Austria. mla: Stock, Miriam. Evolution of a Fungal Pathogen towards Individual versus Social Immunity in Ants. Institute of Science and Technology Austria, 2014. short: M. Stock, Evolution of a Fungal Pathogen towards Individual versus Social Immunity in Ants, Institute of Science and Technology Austria, 2014. corr_author: '1' date_created: 2018-12-11T11:51:49Z date_published: 2014-04-01T00:00:00Z date_updated: 2026-07-29T10:05:33Z day: '01' degree_awarded: PhD department: - _id: SyCr - _id: GradSch doi_confirm: '1' language: - iso: eng month: '04' oa_version: None page: '101' publication_identifier: issn: - 2663-337X publication_status: published publisher: Institute of Science and Technology Austria publist_id: '5803' status: public supervisor: - first_name: Sylvia M full_name: Cremer, Sylvia M id: 2F64EC8C-F248-11E8-B48F-1D18A9856A87 last_name: Cremer orcid: 0000-0002-2193-3868 title: Evolution of a fungal pathogen towards individual versus social immunity in ants type: dissertation user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9 year: '2014' ... --- OA_place: publisher _id: '1402' abstract: - lang: eng text: Phosphatidylinositol (Ptdlns) is a structural phospholipid that can be phosphorylated into various lipid signaling molecules, designated polyphosphoinositides (PPIs). The reversible phosphorylation of PPIs on the 3, 4, or 5 position of inositol is performed by a set of organelle-specific kinases and phosphatases, and the characteristic head groups make these molecules ideal for regulating biological processes in time and space. In yeast and mammals, Ptdlns3P and Ptdlns(3,5)P2 play crucial roles in trafficking toward the lytic compartments, whereas the role in plants is not yet fully understood. Here we identified the role of a land plant-specific subgroup of PPI phosphatases, the suppressor of actin 2 (SAC2) to SAC5, during vauolar trafficking and morphogenesis in Arabidopsis thaliana. SAC2-SAC5 localize to the tonoplast along with Ptdlns3P, the presumable product of their activity. in SAC gain- and loss-of-function mutants, the levels of Ptdlns monophosphates and bisphosphates were changed, with opposite effects on the morphology of storage and lytic vacuoles, and the trafficking toward the vacuoles was defective. Moreover, multiple sac knockout mutants had an increased number of smaller storage and lytic vacuoles, whereas extralarge vacuoles were observed in the overexpression lines, correlating with various growth and developmental defects. The fragmented vacuolar phenotype of sac mutants could be mimicked by treating wild-type seedlings with Ptdlns(3,5)P2, corroborating that this PPI is important for vacuole morphology. Taken together, these results provide evidence that PPIs, together with their metabolic enzymes SAC2-SAC5, are crucial for vacuolar trafficking and for vacuolar morphology and function in plants. alternative_title: - ISTA Thesis article_processing_charge: No author: - first_name: Petra full_name: Marhavá, Petra id: 44E59624-F248-11E8-B48F-1D18A9856A87 last_name: Marhavá citation: ama: Marhavá P. Molecular mechanisms of patterning and subcellular trafficking in Arabidopsis thaliana. 2014. apa: Marhavá, P. (2014). Molecular mechanisms of patterning and subcellular trafficking in Arabidopsis thaliana. Institute of Science and Technology Austria. chicago: Marhavá, Petra. “Molecular Mechanisms of Patterning and Subcellular Trafficking in Arabidopsis Thaliana.” Institute of Science and Technology Austria, 2014. ieee: P. Marhavá, “Molecular mechanisms of patterning and subcellular trafficking in Arabidopsis thaliana,” Institute of Science and Technology Austria, 2014. ista: Marhavá P. 2014. Molecular mechanisms of patterning and subcellular trafficking in Arabidopsis thaliana. Institute of Science and Technology Austria. mla: Marhavá, Petra. Molecular Mechanisms of Patterning and Subcellular Trafficking in Arabidopsis Thaliana. Institute of Science and Technology Austria, 2014. short: P. Marhavá, Molecular Mechanisms of Patterning and Subcellular Trafficking in Arabidopsis Thaliana, Institute of Science and Technology Austria, 2014. corr_author: '1' date_created: 2018-12-11T11:51:49Z date_published: 2014-12-01T00:00:00Z date_updated: 2026-07-29T10:06:44Z day: '01' degree_awarded: PhD department: - _id: JiFr - _id: GradSch doi_confirm: '1' language: - iso: eng month: '12' oa_version: None page: '90' publication_identifier: issn: - 2663-337X publication_status: published publisher: Institute of Science and Technology Austria publist_id: '5805' status: public supervisor: - first_name: Jiří full_name: Friml, Jiří id: 4159519E-F248-11E8-B48F-1D18A9856A87 last_name: Friml orcid: 0000-0002-8302-7596 title: Molecular mechanisms of patterning and subcellular trafficking in Arabidopsis thaliana type: dissertation user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9 year: '2014' ... --- OA_place: publisher _id: '1403' abstract: - lang: eng text: A variety of developmental and disease related processes depend on epithelial cell sheet spreading. In order to gain insight into the biophysical mechanism(s) underlying the tissue morphogenesis we studied the spreading of an epithelium during the early development of the zebrafish embryo. In zebrafish epiboly the enveloping cell layer (EVL), a simple squamous epithelium, spreads over the yolk cell to completely engulf it at the end of gastrulation. Previous studies have proposed that an actomyosin ring forming within the yolk syncytial layer (YSL) acts as purse string that through constriction along its circumference pulls on the margin of the EVL. Direct biophysical evidence for this hypothesis has however been missing. The aim of the thesis was to understand how the actomyosin ring may generate pulling forces onto the EVL and what cellular mechanism(s) may facilitate the spreading of the epithelium. Using laser ablation to measure cortical tension within the actomyosin ring we found an anisotropic tension distribution, which was highest along the circumference of the ring. However the low degree of anisotropy was incompatible with the actomyosin ring functioning as a purse string only. Additionally, we observed retrograde cortical flow from vegetal parts of the ring into the EVL margin. Interpreting the experimental data using a theoretical distribution that models the tissues as active viscous gels led us to proposen that the actomyosin ring has a twofold contribution to EVL epiboly. It not only acts as a purse string through constriction along its circumference, but in addition constriction along the width of the ring generates pulling forces through friction-resisted cortical flow. Moreover, when rendering the purse string mechanism unproductive EVL epiboly proceeded normally indicating that the flow-friction mechanism is sufficient to drive the process. Aiming to understand what cellular mechanism(s) may facilitate the spreading of the epithelium we found that tension-oriented EVL cell divisions limit tissue anisotropy by releasing tension along the division axis and promote epithelial spreading. Notably, EVL cells undergo ectopic cell fusion in conditions in which oriented-cell division is impaired or the epithelium is mechanically challenged. Taken together our study of EVL epiboly suggests a novel mechanism of force generation for actomyosin rings through friction-resisted cortical flow and highlights the importance of tension-oriented cell divisions in epithelial morphogenesis. acknowledged_ssus: - _id: SSU alternative_title: - ISTA Thesis article_processing_charge: No author: - first_name: Martin full_name: Behrndt, Martin id: 3ECECA3A-F248-11E8-B48F-1D18A9856A87 last_name: Behrndt citation: ama: Behrndt M. Forces driving epithelial spreading in zebrafish epiboly. 2014. apa: Behrndt, M. (2014). Forces driving epithelial spreading in zebrafish epiboly. Institute of Science and Technology Austria. chicago: Behrndt, Martin. “Forces Driving Epithelial Spreading in Zebrafish Epiboly.” Institute of Science and Technology Austria, 2014. ieee: M. Behrndt, “Forces driving epithelial spreading in zebrafish epiboly,” Institute of Science and Technology Austria, 2014. ista: Behrndt M. 2014. Forces driving epithelial spreading in zebrafish epiboly. Institute of Science and Technology Austria. mla: Behrndt, Martin. Forces Driving Epithelial Spreading in Zebrafish Epiboly. Institute of Science and Technology Austria, 2014. short: M. Behrndt, Forces Driving Epithelial Spreading in Zebrafish Epiboly, Institute of Science and Technology Austria, 2014. corr_author: '1' date_created: 2018-12-11T11:51:49Z date_published: 2014-08-01T00:00:00Z date_updated: 2026-07-29T10:07:19Z day: '01' ddc: - '590' degree_awarded: PhD department: - _id: CaHe - _id: GradSch doi_confirm: '1' file: - access_level: closed checksum: 67df5501b1b5b313c3bf9a360d713693 content_type: application/pdf creator: cchlebak date_created: 2026-03-09T14:53:14Z date_updated: 2026-03-09T14:53:14Z file_id: '21421' file_name: 2014 Behrnd final.pdf file_size: 24842978 relation: main_file file_date_updated: 2026-03-09T14:53:14Z has_accepted_license: '1' language: - iso: eng month: '08' oa_version: None page: '91' publication_identifier: issn: - 2663-337X publication_status: published publisher: Institute of Science and Technology Austria publist_id: '5804' related_material: record: - id: '2282' relation: part_of_dissertation status: public - id: '2950' relation: part_of_dissertation status: public - id: '3373' relation: part_of_dissertation status: public status: public supervisor: - first_name: Carl-Philipp J full_name: Heisenberg, Carl-Philipp J id: 39427864-F248-11E8-B48F-1D18A9856A87 last_name: Heisenberg orcid: 0000-0002-0912-4566 title: Forces driving epithelial spreading in zebrafish epiboly type: dissertation user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9 year: '2014' ... --- _id: '2255' abstract: - lang: eng text: Motivated by applications in biology, we present an algorithm for estimating the length of tube-like shapes in 3-dimensional Euclidean space. In a first step, we combine the tube formula of Weyl with integral geometric methods to obtain an integral representation of the length, which we approximate using a variant of the Koksma-Hlawka Theorem. In a second step, we use tools from computational topology to decrease the dependence on small perturbations of the shape. We present computational experiments that shed light on the stability and the convergence rate of our algorithm. article_processing_charge: No author: - first_name: Herbert full_name: Edelsbrunner, Herbert id: 3FB178DA-F248-11E8-B48F-1D18A9856A87 last_name: Edelsbrunner orcid: 0000-0002-9823-6833 - first_name: Florian full_name: Pausinger, Florian id: 2A77D7A2-F248-11E8-B48F-1D18A9856A87 last_name: Pausinger orcid: 0000-0002-8379-3768 citation: ama: Edelsbrunner H, Pausinger F. Stable length estimates of tube-like shapes. Journal of Mathematical Imaging and Vision. 2014;50(1):164-177. doi:10.1007/s10851-013-0468-x apa: Edelsbrunner, H., & Pausinger, F. (2014). Stable length estimates of tube-like shapes. Journal of Mathematical Imaging and Vision. Springer. https://doi.org/10.1007/s10851-013-0468-x chicago: Edelsbrunner, Herbert, and Florian Pausinger. “Stable Length Estimates of Tube-like Shapes.” Journal of Mathematical Imaging and Vision. Springer, 2014. https://doi.org/10.1007/s10851-013-0468-x. ieee: H. Edelsbrunner and F. Pausinger, “Stable length estimates of tube-like shapes,” Journal of Mathematical Imaging and Vision, vol. 50, no. 1. Springer, pp. 164–177, 2014. ista: Edelsbrunner H, Pausinger F. 2014. Stable length estimates of tube-like shapes. Journal of Mathematical Imaging and Vision. 50(1), 164–177. mla: Edelsbrunner, Herbert, and Florian Pausinger. “Stable Length Estimates of Tube-like Shapes.” Journal of Mathematical Imaging and Vision, vol. 50, no. 1, Springer, 2014, pp. 164–77, doi:10.1007/s10851-013-0468-x. short: H. Edelsbrunner, F. Pausinger, Journal of Mathematical Imaging and Vision 50 (2014) 164–177. corr_author: '1' date_created: 2018-12-11T11:56:36Z date_published: 2014-09-01T00:00:00Z date_updated: 2026-07-29T10:08:33Z day: '01' ddc: - '000' department: - _id: HeEd doi: 10.1007/s10851-013-0468-x ec_funded: 1 external_id: isi: - '000339823000012' file: - access_level: open_access checksum: 2f93f3e63a38a85cd4404d7953913b14 content_type: application/pdf creator: system date_created: 2018-12-12T10:16:18Z date_updated: 2020-07-14T12:45:35Z file_id: '5204' file_name: IST-2016-549-v1+1_2014-J-06-LengthEstimate.pdf file_size: 3941391 relation: main_file file_date_updated: 2020-07-14T12:45:35Z fulldoi: https://doi.org/10.1007/s10851-013-0468-x has_accepted_license: '1' intvolume: ' 50' isi: 1 issue: '1' language: - iso: eng month: '09' oa: 1 oa_version: Submitted Version page: 164 - 177 project: - _id: 255D761E-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '318493' name: Topological Complex Systems publication: Journal of Mathematical Imaging and Vision publication_identifier: issn: - 0924-9907 publication_status: published publisher: Springer publist_id: '4691' pubrep_id: '549' quality_controlled: '1' related_material: record: - id: '2843' relation: earlier_version status: public - id: '1399' relation: dissertation_contains status: public scopus_import: '1' status: public title: Stable length estimates of tube-like shapes type: journal_article user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd volume: 50 year: '2014' ... --- _id: '2159' abstract: - lang: eng text: 'Motivated by topological Tverberg-type problems, we consider multiple (double, triple, and higher multiplicity) selfintersection points of maps from finite simplicial complexes (compact polyhedra) into ℝd and study conditions under which such multiple points can be eliminated. The most classical case is that of embeddings (i.e., maps without double points) of a κ-dimensional complex K into ℝ2κ. For this problem, the work of van Kampen, Shapiro, and Wu provides an efficiently testable necessary condition for embeddability (namely, vanishing of the van Kampen ob-struction). For κ ≥ 3, the condition is also sufficient, and yields a polynomial-time algorithm for deciding embeddability: One starts with an arbitrary map f : K→ℝ2κ, which generically has finitely many double points; if k ≥ 3 and if the obstruction vanishes then one can successively remove these double points by local modifications of the map f. One of the main tools is the famous Whitney trick that permits eliminating pairs of double points of opposite intersection sign. We are interested in generalizing this approach to intersection points of higher multiplicity. We call a point y 2 ℝd an r-fold Tverberg point of a map f : Kκ →ℝd if y lies in the intersection f(σ1)∩. ∩f(σr) of the images of r pairwise disjoint simplices of K. The analogue of (non-)embeddability that we study is the problem Tverbergκ r→d: Given a κ-dimensional complex K, does it satisfy a Tverberg-type theorem with parameters r and d, i.e., does every map f : K κ → ℝd have an r-fold Tverberg point? Here, we show that for fixed r, κ and d of the form d = rm and k = (r-1)m, m ≥ 3, there is a polynomial-time algorithm for deciding this (based on the vanishing of a cohomological obstruction, as in the case of embeddings). Our main tool is an r-fold analogue of the Whitney trick: Given r pairwise disjoint simplices of K such that the intersection of their images contains two r-fold Tverberg points y+ and y- of opposite intersection sign, we can eliminate y+ and y- by a local isotopy of f. In a subsequent paper, we plan to develop this further and present a generalization of the classical Haeiger-Weber Theorem (which yields a necessary and sufficient condition for embeddability of κ-complexes into ℝd for a wider range of dimensions) to intersection points of higher multiplicity.' acknowledgement: Swiss National Science Foundation (Project SNSF-PP00P2-138948) author: - first_name: Isaac full_name: Mabillard, Isaac id: 32BF9DAA-F248-11E8-B48F-1D18A9856A87 last_name: Mabillard - first_name: Uli full_name: Wagner, Uli id: 36690CA2-F248-11E8-B48F-1D18A9856A87 last_name: Wagner orcid: 0000-0002-1494-0568 citation: ama: 'Mabillard I, Wagner U. Eliminating Tverberg points, I. An analogue of the Whitney trick. In: Proceedings of the Annual Symposium on Computational Geometry. ACM; 2014:171-180. doi:10.1145/2582112.2582134' apa: 'Mabillard, I., & Wagner, U. (2014). Eliminating Tverberg points, I. An analogue of the Whitney trick. In Proceedings of the Annual Symposium on Computational Geometry (pp. 171–180). Kyoto, Japan: ACM. https://doi.org/10.1145/2582112.2582134' chicago: Mabillard, Isaac, and Uli Wagner. “Eliminating Tverberg Points, I. An Analogue of the Whitney Trick.” In Proceedings of the Annual Symposium on Computational Geometry, 171–80. ACM, 2014. https://doi.org/10.1145/2582112.2582134. ieee: I. Mabillard and U. Wagner, “Eliminating Tverberg points, I. An analogue of the Whitney trick,” in Proceedings of the Annual Symposium on Computational Geometry, Kyoto, Japan, 2014, pp. 171–180. ista: 'Mabillard I, Wagner U. 2014. Eliminating Tverberg points, I. An analogue of the Whitney trick. Proceedings of the Annual Symposium on Computational Geometry. SoCG: Symposium on Computational Geometry, 171–180.' mla: Mabillard, Isaac, and Uli Wagner. “Eliminating Tverberg Points, I. An Analogue of the Whitney Trick.” Proceedings of the Annual Symposium on Computational Geometry, ACM, 2014, pp. 171–80, doi:10.1145/2582112.2582134. short: I. Mabillard, U. Wagner, in:, Proceedings of the Annual Symposium on Computational Geometry, ACM, 2014, pp. 171–180. conference: end_date: 2014-06-11 location: Kyoto, Japan name: 'SoCG: Symposium on Computational Geometry' start_date: 2014-06-08 corr_author: '1' date_created: 2018-12-11T11:56:03Z date_published: 2014-06-08T00:00:00Z date_updated: 2026-07-29T11:26:06Z day: '08' ddc: - '510' department: - _id: UlWa doi: 10.1145/2582112.2582134 file: - access_level: open_access checksum: 2aae223fee8ffeaf57bbabd8d92b6a2c content_type: application/pdf creator: system date_created: 2018-12-12T10:09:12Z date_updated: 2020-07-14T12:45:30Z file_id: '4735' file_name: IST-2016-534-v1+1_Eliminating_Tverberg_points_I._An_analogue_of_the_Whitney_trick.pdf file_size: 914396 relation: main_file file_date_updated: 2020-07-14T12:45:30Z fulldoi: https://doi.org/10.1145/2582112.2582134 has_accepted_license: '1' language: - iso: eng month: '06' oa: 1 oa_version: Submitted Version page: 171 - 180 publication: Proceedings of the Annual Symposium on Computational Geometry publication_status: published publisher: ACM publist_id: '4847' pubrep_id: '534' quality_controlled: '1' related_material: record: - id: '1123' relation: dissertation_contains status: public scopus_import: 1 status: public title: Eliminating Tverberg points, I. An analogue of the Whitney trick type: conference user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87 year: '2014' ...