--- _id: '1335' abstract: - lang: eng text: In this paper we review various automata-theoretic formalisms for expressing quantitative properties. We start with finite-state Boolean automata that express the traditional regular properties. We then consider weighted ω-automata that can measure the average density of events, which finite-state Boolean automata cannot. However, even weighted ω-automata cannot express basic performance properties like average response time. We finally consider two formalisms of weighted ω-automata with monitors, where the monitors are either (a) counters or (b) weighted automata themselves. We present a translation result to establish that these two formalisms are equivalent. Weighted ω-automata with monitors generalize weighted ω-automata, and can express average response time property. They present a natural, robust, and expressive framework for quantitative specifications, with important decidable properties. 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 - 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. Quantitative monitor automata. In: Vol 9837. Springer; 2016:23-38. doi:10.1007/978-3-662-53413-7_2' apa: 'Chatterjee, K., Henzinger, T. A., & Otop, J. (2016). Quantitative monitor automata (Vol. 9837, pp. 23–38). Presented at the SAS: Static Analysis Symposium, Edinburgh, United Kingdom: Springer. https://doi.org/10.1007/978-3-662-53413-7_2' chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Quantitative Monitor Automata,” 9837:23–38. Springer, 2016. https://doi.org/10.1007/978-3-662-53413-7_2. ieee: 'K. Chatterjee, T. A. Henzinger, and J. Otop, “Quantitative monitor automata,” presented at the SAS: Static Analysis Symposium, Edinburgh, United Kingdom, 2016, vol. 9837, pp. 23–38.' ista: 'Chatterjee K, Henzinger TA, Otop J. 2016. Quantitative monitor automata. SAS: Static Analysis Symposium, LNCS, vol. 9837, 23–38.' mla: Chatterjee, Krishnendu, et al. Quantitative Monitor Automata. Vol. 9837, Springer, 2016, pp. 23–38, doi:10.1007/978-3-662-53413-7_2. short: K. Chatterjee, T.A. Henzinger, J. Otop, in:, Springer, 2016, pp. 23–38. conference: end_date: 2016-09-10 location: Edinburgh, United Kingdom name: 'SAS: Static Analysis Symposium' start_date: 2016-09-08 date_created: 2018-12-11T11:51:26Z date_published: 2016-08-31T00:00:00Z date_updated: 2021-01-12T06:49:58Z day: '31' department: - _id: KrCh - _id: ToHe doi: 10.1007/978-3-662-53413-7_2 ec_funded: 1 intvolume: ' 9837' language: - iso: eng main_file_link: - open_access: '1' url: https://arxiv.org/abs/1604.06764 month: '08' oa: 1 oa_version: Preprint page: 23 - 38 project: - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 25F42A32-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: Z211 name: The Wittgenstein Prize - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 25892FC0-B435-11E9-9278-68D0E5697425 grant_number: ICT15-003 name: Efficient Algorithms for Computer Aided Verification publication_status: published publisher: Springer publist_id: '5932' quality_controlled: '1' scopus_import: 1 status: public title: Quantitative monitor automata type: conference user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87 volume: 9837 year: '2016' ... --- _id: '1340' abstract: - lang: eng text: We study repeated games with absorbing states, a type of two-player, zero-sum concurrent mean-payoff games with the prototypical example being the Big Match of Gillete (1957). These games may not allow optimal strategies but they always have ε-optimal strategies. In this paper we design ε-optimal strategies for Player 1 in these games that use only O(log log T) space. Furthermore, we construct strategies for Player 1 that use space s(T), for an arbitrary small unbounded non-decreasing function s, and which guarantee an ε-optimal value for Player 1 in the limit superior sense. The previously known strategies use space Ω(log T) and it was known that no strategy can use constant space if it is ε-optimal even in the limit superior sense. We also give a complementary lower bound. Furthermore, we also show that no Markov strategy, even extended with finite memory, can ensure value greater than 0 in the Big Match, answering a question posed by Neyman [11]. alternative_title: - LNCS author: - first_name: Kristoffer full_name: Hansen, Kristoffer last_name: Hansen - first_name: Rasmus full_name: Ibsen-Jensen, Rasmus id: 3B699956-F248-11E8-B48F-1D18A9856A87 last_name: Ibsen-Jensen orcid: 0000-0003-4783-0389 - first_name: Michal full_name: Koucký, Michal last_name: Koucký citation: ama: 'Hansen K, Ibsen-Jensen R, Koucký M. The big match in small space. In: Vol 9928. Springer; 2016:64-76. doi:10.1007/978-3-662-53354-3_6' apa: 'Hansen, K., Ibsen-Jensen, R., & Koucký, M. (2016). The big match in small space (Vol. 9928, pp. 64–76). Presented at the SAGT: Symposium on Algorithmic Game Theory, Liverpool, United Kingdom: Springer. https://doi.org/10.1007/978-3-662-53354-3_6' chicago: Hansen, Kristoffer, Rasmus Ibsen-Jensen, and Michal Koucký. “The Big Match in Small Space,” 9928:64–76. Springer, 2016. https://doi.org/10.1007/978-3-662-53354-3_6. ieee: 'K. Hansen, R. Ibsen-Jensen, and M. Koucký, “The big match in small space,” presented at the SAGT: Symposium on Algorithmic Game Theory, Liverpool, United Kingdom, 2016, vol. 9928, pp. 64–76.' ista: 'Hansen K, Ibsen-Jensen R, Koucký M. 2016. The big match in small space. SAGT: Symposium on Algorithmic Game Theory, LNCS, vol. 9928, 64–76.' mla: Hansen, Kristoffer, et al. The Big Match in Small Space. Vol. 9928, Springer, 2016, pp. 64–76, doi:10.1007/978-3-662-53354-3_6. short: K. Hansen, R. Ibsen-Jensen, M. Koucký, in:, Springer, 2016, pp. 64–76. conference: end_date: 2016-09-21 location: Liverpool, United Kingdom name: 'SAGT: Symposium on Algorithmic Game Theory' start_date: 2016-09-19 date_created: 2018-12-11T11:51:28Z date_published: 2016-09-01T00:00:00Z date_updated: 2021-01-12T06:50:00Z day: '01' department: - _id: KrCh doi: 10.1007/978-3-662-53354-3_6 ec_funded: 1 intvolume: ' 9928' language: - iso: eng main_file_link: - open_access: '1' url: https://arxiv.org/abs/1604.07634 month: '09' oa: 1 oa_version: Preprint page: 64 - 76 project: - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 25892FC0-B435-11E9-9278-68D0E5697425 grant_number: ICT15-003 name: Efficient Algorithms for Computer Aided Verification - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' publication_status: published publisher: Springer publist_id: '5927' quality_controlled: '1' scopus_import: 1 status: public title: The big match in small space type: conference user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87 volume: 9928 year: '2016' ... --- _id: '1380' abstract: - lang: eng text: We consider higher-dimensional versions of Kannan and Lipton's Orbit Problem - determining whether a target vector space V may be reached from a starting point x under repeated applications of a linear transformation A. Answering two questions posed by Kannan and Lipton in the 1980s, we show that when V has dimension one, this problem is solvable in polynomial time, and when V has dimension two or three, the problem is in NPRP. article_number: '23' author: - first_name: Ventsislav K full_name: Chonev, Ventsislav K id: 36CBE2E6-F248-11E8-B48F-1D18A9856A87 last_name: Chonev - first_name: Joël full_name: Ouaknine, Joël last_name: Ouaknine - first_name: James full_name: Worrell, James last_name: Worrell citation: ama: Chonev VK, Ouaknine J, Worrell J. On the complexity of the orbit problem. Journal of the ACM. 2016;63(3). doi:10.1145/2857050 apa: Chonev, V. K., Ouaknine, J., & Worrell, J. (2016). On the complexity of the orbit problem. Journal of the ACM. ACM. https://doi.org/10.1145/2857050 chicago: Chonev, Ventsislav K, Joël Ouaknine, and James Worrell. “On the Complexity of the Orbit Problem.” Journal of the ACM. ACM, 2016. https://doi.org/10.1145/2857050. ieee: V. K. Chonev, J. Ouaknine, and J. Worrell, “On the complexity of the orbit problem,” Journal of the ACM, vol. 63, no. 3. ACM, 2016. ista: Chonev VK, Ouaknine J, Worrell J. 2016. On the complexity of the orbit problem. Journal of the ACM. 63(3), 23. mla: Chonev, Ventsislav K., et al. “On the Complexity of the Orbit Problem.” Journal of the ACM, vol. 63, no. 3, 23, ACM, 2016, doi:10.1145/2857050. short: V.K. Chonev, J. Ouaknine, J. Worrell, Journal of the ACM 63 (2016). date_created: 2018-12-11T11:51:41Z date_published: 2016-06-01T00:00:00Z date_updated: 2021-01-12T06:50:17Z day: '01' department: - _id: KrCh doi: 10.1145/2857050 intvolume: ' 63' issue: '3' language: - iso: eng main_file_link: - open_access: '1' url: http://arxiv.org/abs/1303.2981 month: '06' oa: 1 oa_version: Preprint publication: Journal of the ACM publication_status: published publisher: ACM publist_id: '5831' quality_controlled: '1' scopus_import: 1 status: public title: On the complexity of the orbit problem type: journal_article user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87 volume: 63 year: '2016' ... --- _id: '1389' abstract: - lang: eng text: "The continuous evolution of a wide variety of systems, including continous-time Markov chains and linear hybrid automata, can be\r\ndescribed in terms of linear differential equations. In this paper we study the decision problem of whether the solution x(t) of a system of linear differential equations dx/dt = Ax reaches a target halfspace infinitely often. This recurrent reachability problem can\r\nequivalently be formulated as the following Infinite Zeros Problem: does a real-valued function f:R≥0 --> R satisfying a given linear\r\ndifferential equation have infinitely many zeros? Our main decidability result is that if the differential equation has order at most 7, then the Infinite Zeros Problem is decidable. On the other hand, we show that a decision procedure for the Infinite Zeros Problem at order 9 (and above) would entail a major breakthrough in Diophantine Approximation, specifically an algorithm for computing the Lagrange constants of arbitrary real algebraic numbers to arbitrary precision." author: - first_name: Ventsislav K full_name: Chonev, Ventsislav K id: 36CBE2E6-F248-11E8-B48F-1D18A9856A87 last_name: Chonev - first_name: Joël full_name: Ouaknine, Joël last_name: Ouaknine - first_name: James full_name: Worrell, James last_name: Worrell citation: ama: 'Chonev VK, Ouaknine J, Worrell J. On recurrent reachability for continuous linear dynamical systems. In: LICS ’16. IEEE; 2016:515-524. doi:10.1145/2933575.2934548' apa: 'Chonev, V. K., Ouaknine, J., & Worrell, J. (2016). On recurrent reachability for continuous linear dynamical systems. In LICS ’16 (pp. 515–524). New York, NY, USA: IEEE. https://doi.org/10.1145/2933575.2934548' chicago: Chonev, Ventsislav K, Joël Ouaknine, and James Worrell. “On Recurrent Reachability for Continuous Linear Dynamical Systems.” In LICS ’16, 515–24. IEEE, 2016. https://doi.org/10.1145/2933575.2934548. ieee: V. K. Chonev, J. Ouaknine, and J. Worrell, “On recurrent reachability for continuous linear dynamical systems,” in LICS ’16, New York, NY, USA, 2016, pp. 515–524. ista: 'Chonev VK, Ouaknine J, Worrell J. 2016. On recurrent reachability for continuous linear dynamical systems. LICS ’16. LICS: Logic in Computer Science, 515–524.' mla: Chonev, Ventsislav K., et al. “On Recurrent Reachability for Continuous Linear Dynamical Systems.” LICS ’16, IEEE, 2016, pp. 515–24, doi:10.1145/2933575.2934548. short: V.K. Chonev, J. Ouaknine, J. Worrell, in:, LICS ’16, IEEE, 2016, pp. 515–524. conference: end_date: 2018-07-08 location: New York, NY, USA name: 'LICS: Logic in Computer Science' start_date: 2018-07-05 date_created: 2018-12-11T11:51:44Z date_published: 2016-07-05T00:00:00Z date_updated: 2021-01-12T06:50:20Z day: '05' department: - _id: KrCh doi: 10.1145/2933575.2934548 ec_funded: 1 language: - iso: eng main_file_link: - open_access: '1' url: https://arxiv.org/abs/1507.03632 month: '07' oa: 1 oa_version: Preprint page: 515 - 524 project: - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling publication: LICS '16 publication_status: published publisher: IEEE publist_id: '5820' quality_controlled: '1' scopus_import: 1 status: public title: On recurrent reachability for continuous linear dynamical systems type: conference user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87 year: '2016' ... --- _id: '1426' abstract: - lang: eng text: 'Brood parasites exploit their host in order to increase their own fitness. Typically, this results in an arms race between parasite trickery and host defence. Thus, it is puzzling to observe hosts that accept parasitism without any resistance. The ‘mafia’ hypothesis suggests that these hosts accept parasitism to avoid retaliation. Retaliation has been shown to evolve when the hosts condition their response to mafia parasites, who use depredation as a targeted response to rejection. However, it is unclear if acceptance would also emerge when ‘farming’ parasites are present in the population. Farming parasites use depredation to synchronize the timing with the host, destroying mature clutches to force the host to re-nest. Herein, we develop an evolutionary model to analyse the interaction between depredatory parasites and their hosts. We show that coevolutionary cycles between farmers and mafia can still induce host acceptance of brood parasites. However, this equilibrium is unstable and in the long-run the dynamics of this host–parasite interaction exhibits strong oscillations: when farmers are the majority, accepters conditional to mafia (the host will reject first and only accept after retaliation by the parasite) have a higher fitness than unconditional accepters (the host always accepts parasitism). This leads to an increase in mafia parasites’ fitness and in turn induce an optimal environment for accepter hosts.' acknowledgement: C.H. gratefully acknowledges funding by the Schrödinger scholarship of the Austrian Science Fund (FWF) J3475. article_number: '160036' author: - first_name: Maria full_name: Chakra, Maria last_name: Chakra - first_name: Christian full_name: Hilbe, Christian id: 2FDF8F3C-F248-11E8-B48F-1D18A9856A87 last_name: Hilbe orcid: 0000-0001-5116-955X - first_name: Arne full_name: Traulsen, Arne last_name: Traulsen citation: ama: Chakra M, Hilbe C, Traulsen A. Coevolutionary interactions between farmers and mafia induce host acceptance of avian brood parasites. Royal Society Open Science. 2016;3(5). doi:10.1098/rsos.160036 apa: Chakra, M., Hilbe, C., & Traulsen, A. (2016). Coevolutionary interactions between farmers and mafia induce host acceptance of avian brood parasites. Royal Society Open Science. Royal Society, The. https://doi.org/10.1098/rsos.160036 chicago: Chakra, Maria, Christian Hilbe, and Arne Traulsen. “Coevolutionary Interactions between Farmers and Mafia Induce Host Acceptance of Avian Brood Parasites.” Royal Society Open Science. Royal Society, The, 2016. https://doi.org/10.1098/rsos.160036. ieee: M. Chakra, C. Hilbe, and A. Traulsen, “Coevolutionary interactions between farmers and mafia induce host acceptance of avian brood parasites,” Royal Society Open Science, vol. 3, no. 5. Royal Society, The, 2016. ista: Chakra M, Hilbe C, Traulsen A. 2016. Coevolutionary interactions between farmers and mafia induce host acceptance of avian brood parasites. Royal Society Open Science. 3(5), 160036. mla: Chakra, Maria, et al. “Coevolutionary Interactions between Farmers and Mafia Induce Host Acceptance of Avian Brood Parasites.” Royal Society Open Science, vol. 3, no. 5, 160036, Royal Society, The, 2016, doi:10.1098/rsos.160036. short: M. Chakra, C. Hilbe, A. Traulsen, Royal Society Open Science 3 (2016). date_created: 2018-12-11T11:51:57Z date_published: 2016-05-01T00:00:00Z date_updated: 2021-01-12T06:50:39Z day: '01' ddc: - '000' department: - _id: KrCh doi: 10.1098/rsos.160036 file: - access_level: open_access checksum: bf84211b31fe87451e738ba301d729c3 content_type: application/pdf creator: system date_created: 2018-12-12T10:14:49Z date_updated: 2020-07-14T12:44:53Z file_id: '5104' file_name: IST-2016-589-v1+1_160036.full.pdf file_size: 937002 relation: main_file file_date_updated: 2020-07-14T12:44:53Z has_accepted_license: '1' intvolume: ' 3' issue: '5' language: - iso: eng month: '05' oa: 1 oa_version: Published Version publication: Royal Society Open Science publication_status: published publisher: Royal Society, The publist_id: '5776' pubrep_id: '589' quality_controlled: '1' scopus_import: 1 status: public title: Coevolutionary interactions between farmers and mafia induce host acceptance of avian brood parasites tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: journal_article user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87 volume: 3 year: '2016' ...