--- _id: '5410' abstract: - lang: eng text: "Board games, like Tic-Tac-Toe and CONNECT-4, play an important role not only in development of mathematical and logical skills, but also in emotional and social development. In this paper, we address the problem of generating targeted starting positions for such games. This can facilitate new approaches for bringing novice players to mastery, and also leads to discovery of interesting game variants. \r\nOur approach generates starting states of varying hardness levels for player 1 in a two-player board game, given rules of the board game, the desired number of steps required for player 1 to win, and the expertise levels of the two players. Our approach leverages symbolic methods and iterative simulation to efficiently search the extremely large state space. We present experimental results that include discovery of states of varying hardness levels for several simple grid-based board games. Also, the presence of such states for standard game variants like Tic-Tac-Toe on board size 4x4 opens up new games to be played that have not been played for ages since the default start state is heavily biased. " alternative_title: - IST Austria Technical Report author: - first_name: Umair full_name: Ahmed, Umair last_name: Ahmed - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Sumit full_name: Gulwani, Sumit last_name: Gulwani citation: ama: Ahmed U, Chatterjee K, Gulwani S. Automatic Generation of Alternative Starting Positions for Traditional Board Games. IST Austria; 2013. doi:10.15479/AT:IST-2013-146-v1-1 apa: Ahmed, U., Chatterjee, K., & Gulwani, S. (2013). Automatic generation of alternative starting positions for traditional board games. IST Austria. https://doi.org/10.15479/AT:IST-2013-146-v1-1 chicago: Ahmed, Umair, Krishnendu Chatterjee, and Sumit Gulwani. Automatic Generation of Alternative Starting Positions for Traditional Board Games. IST Austria, 2013. https://doi.org/10.15479/AT:IST-2013-146-v1-1. ieee: U. Ahmed, K. Chatterjee, and S. Gulwani, Automatic generation of alternative starting positions for traditional board games. IST Austria, 2013. ista: Ahmed U, Chatterjee K, Gulwani S. 2013. Automatic generation of alternative starting positions for traditional board games, IST Austria, 13p. mla: Ahmed, Umair, et al. Automatic Generation of Alternative Starting Positions for Traditional Board Games. IST Austria, 2013, doi:10.15479/AT:IST-2013-146-v1-1. short: U. Ahmed, K. Chatterjee, S. Gulwani, Automatic Generation of Alternative Starting Positions for Traditional Board Games, IST Austria, 2013. date_created: 2018-12-12T11:39:10Z date_published: 2013-12-03T00:00:00Z date_updated: 2023-02-23T10:00:50Z day: '03' ddc: - '000' - '005' department: - _id: KrCh doi: 10.15479/AT:IST-2013-146-v1-1 file: - access_level: open_access checksum: 409f3aaaf1184e4057b89cbb449dac80 content_type: application/pdf creator: system date_created: 2018-12-12T11:54:06Z date_updated: 2020-07-14T12:46:46Z file_id: '5528' file_name: IST-2013-146-v1+1_main.pdf file_size: 818189 relation: main_file file_date_updated: 2020-07-14T12:46:46Z has_accepted_license: '1' language: - iso: eng month: '12' oa: 1 oa_version: Published Version page: '13' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '146' related_material: record: - id: '1481' relation: later_version status: public status: public title: Automatic generation of alternative starting positions for traditional board games type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2013' ... --- _id: '6440' abstract: - lang: eng text: In order to guarantee that each method of a data structure updates the logical state exactly once, al-most all non-blocking implementations employ Compare-And-Swap (CAS) based synchronization. For FIFO queue implementations this translates into concurrent enqueue or dequeue methods competing among themselves to update the same variable, the tail or the head, respectively, leading to high contention and poor scalability. Recent non-blocking queue implementations try to alleviate high contentionby increasing the number of contention points, all the while using CAS-based synchronization. Furthermore, obtaining a wait-free implementation with competition is achieved by additional synchronization which leads to further degradation of performance.In this paper we formalize the notion of competitiveness of a synchronizing statement which can beused as a measure for the scalability of concurrent implementations. We present a new queue implementation, the Speculative Pairing (SP) queue, which, as we show, decreases competitiveness by using Fetch-And-Increment (FAI) instead of CAS. We prove that the SP queue is linearizable and lock-free.We also show that replacing CAS with FAI leads to wait-freedom for dequeue methods without an adverse effect on performance. In fact, our experiments suggest that the SP queue can perform and scale better than the state-of-the-art queue implementations. alternative_title: - IST Austria Technical Report author: - 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: Hannes full_name: Payer, Hannes last_name: Payer - first_name: Ali full_name: Sezgin, Ali id: 4C7638DA-F248-11E8-B48F-1D18A9856A87 last_name: Sezgin citation: ama: Henzinger TA, Payer H, Sezgin A. Replacing Competition with Cooperation to Achieve Scalable Lock-Free FIFO Queues . IST Austria; 2013. doi:10.15479/AT:IST-2013-124-v1-1 apa: Henzinger, T. A., Payer, H., & Sezgin, A. (2013). Replacing competition with cooperation to achieve scalable lock-free FIFO queues . IST Austria. https://doi.org/10.15479/AT:IST-2013-124-v1-1 chicago: Henzinger, Thomas A, Hannes Payer, and Ali Sezgin. Replacing Competition with Cooperation to Achieve Scalable Lock-Free FIFO Queues . IST Austria, 2013. https://doi.org/10.15479/AT:IST-2013-124-v1-1. ieee: T. A. Henzinger, H. Payer, and A. Sezgin, Replacing competition with cooperation to achieve scalable lock-free FIFO queues . IST Austria, 2013. ista: Henzinger TA, Payer H, Sezgin A. 2013. Replacing competition with cooperation to achieve scalable lock-free FIFO queues , IST Austria, 23p. mla: Henzinger, Thomas A., et al. Replacing Competition with Cooperation to Achieve Scalable Lock-Free FIFO Queues . IST Austria, 2013, doi:10.15479/AT:IST-2013-124-v1-1. short: T.A. Henzinger, H. Payer, A. Sezgin, Replacing Competition with Cooperation to Achieve Scalable Lock-Free FIFO Queues , IST Austria, 2013. date_created: 2019-05-13T14:13:27Z date_published: 2013-06-13T00:00:00Z date_updated: 2020-07-14T23:06:19Z day: '13' ddc: - '000' - '005' department: - _id: ToHe doi: 10.15479/AT:IST-2013-124-v1-1 file: - access_level: open_access checksum: a219ba4eada6cd62befed52262ee15d4 content_type: application/pdf creator: dernst date_created: 2019-05-13T14:11:39Z date_updated: 2020-07-14T12:47:30Z file_id: '6441' file_name: 2013_TechRep_Henzinger.pdf file_size: 549684 relation: main_file file_date_updated: 2020-07-14T12:47:30Z has_accepted_license: '1' language: - iso: eng month: '06' oa: 1 oa_version: Published Version page: '23' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '124' status: public title: 'Replacing competition with cooperation to achieve scalable lock-free FIFO queues ' type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2013' ... --- _id: '5377' abstract: - lang: eng text: 'Two-player games on graphs are central in many problems in formal verification and program analysis such as synthesis and verification of open systems. In this work we consider solving recursive game graphs (or pushdown game graphs) that can model the control flow of sequential programs with recursion. While pushdown games have been studied before with qualitative objectives, such as reachability and ω-regular objectives, in this work we study for the first time such games with the most well-studied quantitative objective, namely, mean-payoff objectives. In pushdown games two types of strategies are relevant: (1) global strategies, that depend on the entire global history; and (2) modular strategies, that have only local memory and thus do not depend on the context of invocation, but only on the history of the current invocation of the module. Our main results are as follows: (1) One-player pushdown games with mean-payoff objectives under global strategies are decidable in polynomial time. (2) Two- player pushdown games with mean-payoff objectives under global strategies are undecidable. (3) One-player pushdown games with mean-payoff objectives under modular strategies are NP- hard. (4) Two-player pushdown games with mean-payoff objectives under modular strategies can be solved in NP (i.e., both one-player and two-player pushdown games with mean-payoff objectives under modular strategies are NP-complete). We also establish the optimal strategy complexity showing that global strategies for mean-payoff objectives require infinite memory even in one-player pushdown games; and memoryless modular strategies are sufficient in two- player pushdown games. Finally we also show that all the problems have the same complexity if the stack boundedness condition is added, where along with the mean-payoff objective the player must also ensure that the stack height is bounded.' 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: Yaron full_name: Velner, Yaron last_name: Velner citation: ama: Chatterjee K, Velner Y. Mean-Payoff Pushdown Games. IST Austria; 2012. doi:10.15479/AT:IST-2012-0002 apa: Chatterjee, K., & Velner, Y. (2012). Mean-payoff pushdown games. IST Austria. https://doi.org/10.15479/AT:IST-2012-0002 chicago: Chatterjee, Krishnendu, and Yaron Velner. Mean-Payoff Pushdown Games. IST Austria, 2012. https://doi.org/10.15479/AT:IST-2012-0002. ieee: K. Chatterjee and Y. Velner, Mean-payoff pushdown games. IST Austria, 2012. ista: Chatterjee K, Velner Y. 2012. Mean-payoff pushdown games, IST Austria, 33p. mla: Chatterjee, Krishnendu, and Yaron Velner. Mean-Payoff Pushdown Games. IST Austria, 2012, doi:10.15479/AT:IST-2012-0002. short: K. Chatterjee, Y. Velner, Mean-Payoff Pushdown Games, IST Austria, 2012. date_created: 2018-12-12T11:38:59Z date_published: 2012-07-02T00:00:00Z date_updated: 2023-02-23T11:05:50Z day: '02' ddc: - '000' - '005' department: - _id: KrCh doi: 10.15479/AT:IST-2012-0002 file: - access_level: open_access checksum: a03c08c1589dbb0c96183a8bcf3ab240 content_type: application/pdf creator: system date_created: 2018-12-12T11:54:00Z date_updated: 2020-07-14T12:46:38Z file_id: '5522' file_name: IST-2012-002_IST-2012-0002.pdf file_size: 592098 relation: main_file file_date_updated: 2020-07-14T12:46:38Z has_accepted_license: '1' language: - iso: eng month: '07' oa: 1 oa_version: Published Version page: '33' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '10' related_material: record: - id: '2956' relation: later_version status: public status: public title: Mean-payoff pushdown games type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2012' ... --- _id: '5378' abstract: - lang: eng text: 'One central issue in the formal design and analysis of reactive systems is the notion of refinement that asks whether all behaviors of the implementation is allowed by the specification. The local interpretation of behavior leads to the notion of simulation. Alternating transition systems (ATSs) provide a general model for composite reactive systems, and the simulation relation for ATSs is known as alternating simulation. The simulation relation for fair transition systems is called fair simulation. In this work our main contributions are as follows: (1) We present an improved algorithm for fair simulation with Büchi fairness constraints; our algorithm requires O(n3 · m) time as compared to the previous known O(n6)-time algorithm, where n is the number of states and m is the number of transitions. (2) We present a game based algorithm for alternating simulation that requires O(m2)-time as compared to the previous known O((n · m)2)-time algorithm, where n is the number of states and m is the size of transition relation. (3) We present an iterative algorithm for alternating simulation that matches the time complexity of the game based algorithm, but is more space efficient than the game based algorithm.' 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: Siddhesh full_name: Chaubal, Siddhesh last_name: Chaubal - first_name: Pritish full_name: Kamath, Pritish last_name: Kamath citation: ama: Chatterjee K, Chaubal S, Kamath P. Faster Algorithms for Alternating Refinement Relations. IST Austria; 2012. doi:10.15479/AT:IST-2012-0001 apa: Chatterjee, K., Chaubal, S., & Kamath, P. (2012). Faster algorithms for alternating refinement relations. IST Austria. https://doi.org/10.15479/AT:IST-2012-0001 chicago: Chatterjee, Krishnendu, Siddhesh Chaubal, and Pritish Kamath. Faster Algorithms for Alternating Refinement Relations. IST Austria, 2012. https://doi.org/10.15479/AT:IST-2012-0001. ieee: K. Chatterjee, S. Chaubal, and P. Kamath, Faster algorithms for alternating refinement relations. IST Austria, 2012. ista: Chatterjee K, Chaubal S, Kamath P. 2012. Faster algorithms for alternating refinement relations, IST Austria, 21p. mla: Chatterjee, Krishnendu, et al. Faster Algorithms for Alternating Refinement Relations. IST Austria, 2012, doi:10.15479/AT:IST-2012-0001. short: K. Chatterjee, S. Chaubal, P. Kamath, Faster Algorithms for Alternating Refinement Relations, IST Austria, 2012. date_created: 2018-12-12T11:38:59Z date_published: 2012-07-04T00:00:00Z date_updated: 2023-02-23T12:21:38Z day: '04' ddc: - '000' - '005' department: - _id: KrCh doi: 10.15479/AT:IST-2012-0001 file: - access_level: open_access checksum: ec8d1857cc7095d3de5107a0162ced37 content_type: application/pdf creator: system date_created: 2018-12-12T11:53:28Z date_updated: 2020-07-14T12:46:39Z file_id: '5489' file_name: IST-2012-0001_IST-2012-0001.pdf file_size: 394256 relation: main_file file_date_updated: 2020-07-14T12:46:39Z has_accepted_license: '1' language: - iso: eng month: '07' oa: 1 oa_version: Published Version page: '21' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '14' related_material: record: - id: '497' relation: later_version status: public status: public title: Faster algorithms for alternating refinement relations type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2012' ... --- _id: '5396' abstract: - lang: eng text: We consider the problem of inference in agraphical model with binary variables. While in theory it is arguably preferable to compute marginal probabilities, in practice researchers often use MAP inference due to the availability of efficient discrete optimization algorithms. We bridge the gap between the two approaches by introducing the Discrete Marginals technique in which approximate marginals are obtained by minimizing an objective function with unary and pair-wise terms over a discretized domain. This allows the use of techniques originally devel-oped for MAP-MRF inference and learning. We explore two ways to set up the objective function - by discretizing the Bethe free energy and by learning it from training data. Experimental results show that for certain types of graphs a learned function can out-perform the Bethe approximation. We also establish a link between the Bethe free energy and submodular functions. alternative_title: - IST Austria Technical Report author: - first_name: Filip full_name: Korc, Filip id: 476A2FD6-F248-11E8-B48F-1D18A9856A87 last_name: Korc - first_name: Vladimir full_name: Kolmogorov, Vladimir id: 3D50B0BA-F248-11E8-B48F-1D18A9856A87 last_name: Kolmogorov - first_name: Christoph full_name: Lampert, Christoph id: 40C20FD2-F248-11E8-B48F-1D18A9856A87 last_name: Lampert orcid: 0000-0001-8622-7887 citation: ama: Korc F, Kolmogorov V, Lampert C. Approximating Marginals Using Discrete Energy Minimization. IST Austria; 2012. doi:10.15479/AT:IST-2012-0003 apa: Korc, F., Kolmogorov, V., & Lampert, C. (2012). Approximating marginals using discrete energy minimization. IST Austria. https://doi.org/10.15479/AT:IST-2012-0003 chicago: Korc, Filip, Vladimir Kolmogorov, and Christoph Lampert. Approximating Marginals Using Discrete Energy Minimization. IST Austria, 2012. https://doi.org/10.15479/AT:IST-2012-0003. ieee: F. Korc, V. Kolmogorov, and C. Lampert, Approximating marginals using discrete energy minimization. IST Austria, 2012. ista: Korc F, Kolmogorov V, Lampert C. 2012. Approximating marginals using discrete energy minimization, IST Austria, 13p. mla: Korc, Filip, et al. Approximating Marginals Using Discrete Energy Minimization. IST Austria, 2012, doi:10.15479/AT:IST-2012-0003. short: F. Korc, V. Kolmogorov, C. Lampert, Approximating Marginals Using Discrete Energy Minimization, IST Austria, 2012. date_created: 2018-12-12T11:39:06Z date_published: 2012-07-23T00:00:00Z date_updated: 2023-02-23T11:13:22Z day: '23' ddc: - '000' department: - _id: VlKo - _id: ChLa doi: 10.15479/AT:IST-2012-0003 file: - access_level: open_access checksum: 7e0ba85ad123b13223aaf6cdde2d288c content_type: application/pdf creator: system date_created: 2018-12-12T11:53:29Z date_updated: 2020-07-14T12:46:44Z file_id: '5490' file_name: IST-2012-0003_IST-2012-0003.pdf file_size: 618744 relation: main_file file_date_updated: 2020-07-14T12:46:44Z has_accepted_license: '1' language: - iso: eng month: '07' oa: 1 oa_version: Published Version page: '13' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '36' related_material: record: - id: '3124' relation: earlier_version status: public status: public title: Approximating marginals using discrete energy minimization type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2012' ...