@misc{9844, author = {Nikolic, Nela and Schreiber, Frank and Dal Co, Alma and Kiviet, Daniel and Bergmiller, Tobias and Littmann, Sten and Kuypers, Marcel and Ackermann, Martin}, publisher = {Public Library of Science}, title = {{Source data for figures and tables}}, doi = {10.1371/journal.pgen.1007122.s018}, year = {2017}, } @inproceedings{12905, author = {Schlögl, Alois and Kiss, Janos}, booktitle = {AHPC17 – Austrian HPC Meeting 2017}, location = {Grundlsee, Austria}, pages = {28}, publisher = {FSP Scientific Computing}, title = {{Scientific Computing at IST Austria}}, year = {2017}, } @inproceedings{13160, abstract = {Transforming deterministic ω -automata into deterministic parity automata is traditionally done using variants of appearance records. We present a more efficient variant of this approach, tailored to Rabin automata, and several optimizations applicable to all appearance records. We compare the methods experimentally and find out that our method produces smaller automata than previous approaches. Moreover, the experiments demonstrate the potential of our method for LTL synthesis, using LTL-to-Rabin translators. It leads to significantly smaller parity automata when compared to state-of-the-art approaches on complex formulae.}, author = {Kretinsky, Jan and Meggendorfer, Tobias and Waldmann, Clara and Weininger, Maximilian}, booktitle = {Tools and Algorithms for the Construction and Analysis of Systems}, isbn = {9783662545768}, issn = {1611-3349}, location = {Uppsala, Sweden}, pages = {443--460}, publisher = {Springer}, title = {{Index appearance record for transforming Rabin automata into parity automata}}, doi = {10.1007/978-3-662-54577-5_26}, volume = {10205}, year = {2017}, } @inproceedings{950, abstract = {Two-player games on graphs are widely studied in formal methods as they model the interaction between a system and its environment. The game is played by moving a token throughout a graph to produce an infinite path. There are several common modes to determine how the players move the token through the graph; e.g., in turn-based games the players alternate turns in moving the token. We study the bidding mode of moving the token, which, to the best of our knowledge, has never been studied in infinite-duration games. Both players have separate budgets, which sum up to $1$. In each turn, a bidding takes place. Both players submit bids simultaneously, and a bid is legal if it does not exceed the available budget. The winner of the bidding pays his bid to the other player and moves the token. For reachability objectives, repeated bidding games have been studied and are called Richman games. There, a central question is the existence and computation of threshold budgets; namely, a value t\in [0,1] such that if\PO's budget exceeds $t$, he can win the game, and if\PT's budget exceeds 1-t, he can win the game. We focus on parity games and mean-payoff games. We show the existence of threshold budgets in these games, and reduce the problem of finding them to Richman games. We also determine the strategy-complexity of an optimal strategy. Our most interesting result shows that memoryless strategies suffice for mean-payoff bidding games. }, author = {Avni, Guy and Henzinger, Thomas A and Chonev, Ventsislav K}, issn = {1868-8969}, location = {Berlin, Germany}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Infinite-duration bidding games}}, doi = {10.4230/LIPIcs.CONCUR.2017.21}, volume = {85}, year = {2017}, } @inproceedings{683, abstract = {Given a triangulation of a point set in the plane, a flip deletes an edge e whose removal leaves a convex quadrilateral, and replaces e by the opposite diagonal of the quadrilateral. It is well known that any triangulation of a point set can be reconfigured to any other triangulation by some sequence of flips. We explore this question in the setting where each edge of a triangulation has a label, and a flip transfers the label of the removed edge to the new edge. It is not true that every labelled triangulation of a point set can be reconfigured to every other labelled triangulation via a sequence of flips, but we characterize when this is possible. There is an obvious necessary condition: for each label l, if edge e has label l in the first triangulation and edge f has label l in the second triangulation, then there must be some sequence of flips that moves label l from e to f, ignoring all other labels. Bose, Lubiw, Pathak and Verdonschot formulated the Orbit Conjecture, which states that this necessary condition is also sufficient, i.e. that all labels can be simultaneously mapped to their destination if and only if each label individually can be mapped to its destination. We prove this conjecture. Furthermore, we give a polynomial-time algorithm to find a sequence of flips to reconfigure one labelled triangulation to another, if such a sequence exists, and we prove an upper bound of O(n7) on the length of the flip sequence. Our proof uses the topological result that the sets of pairwise non-crossing edges on a planar point set form a simplicial complex that is homeomorphic to a high-dimensional ball (this follows from a result of Orden and Santos; we give a different proof based on a shelling argument). The dual cell complex of this simplicial ball, called the flip complex, has the usual flip graph as its 1-skeleton. We use properties of the 2-skeleton of the flip complex to prove the Orbit Conjecture.}, author = {Lubiw, Anna and Masárová, Zuzana and Wagner, Uli}, location = {Brisbane, Australia}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{A proof of the orbit conjecture for flipping edge labelled triangulations}}, doi = {10.4230/LIPIcs.SoCG.2017.49}, volume = {77}, year = {2017}, }