@inproceedings{8600, abstract = {A vector addition system with states (VASS) consists of a finite set of states and counters. A transition changes the current state to the next state, and every counter is either incremented, or decremented, or left unchanged. A state and value for each counter is a configuration; and a computation is an infinite sequence of configurations with transitions between successive configurations. A probabilistic VASS consists of a VASS along with a probability distribution over the transitions for each state. Qualitative properties such as state and configuration reachability have been widely studied for VASS. In this work we consider multi-dimensional long-run average objectives for VASS and probabilistic VASS. For a counter, the cost of a configuration is the value of the counter; and the long-run average value of a computation for the counter is the long-run average of the costs of the configurations in the computation. The multi-dimensional long-run average problem given a VASS and a threshold value for each counter, asks whether there is a computation such that for each counter the long-run average value for the counter does not exceed the respective threshold. For probabilistic VASS, instead of the existence of a computation, we consider whether the expected long-run average value for each counter does not exceed the respective threshold. Our main results are as follows: we show that the multi-dimensional long-run average problem (a) is NP-complete for integer-valued VASS; (b) is undecidable for natural-valued VASS (i.e., nonnegative counters); and (c) can be solved in polynomial time for probabilistic integer-valued VASS, and probabilistic natural-valued VASS when all computations are non-terminating.}, author = {Chatterjee, Krishnendu and Henzinger, Thomas A and Otop, Jan}, booktitle = {31st International Conference on Concurrency Theory}, isbn = {9783959771603}, issn = {18688969}, location = {Virtual}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Multi-dimensional long-run average problems for vector addition systems with states}}, doi = {10.4230/LIPIcs.CONCUR.2020.23}, volume = {171}, year = {2020}, } @inproceedings{8599, abstract = {A graph game is a two-player zero-sum game in which the players move a token throughout a graph to produce an infinite path, which determines the winner or payoff of the game. In bidding games, both players have budgets, and in each turn, we hold an "auction" (bidding) to determine which player moves the token. In this survey, we consider several bidding mechanisms and study their effect on the properties of the game. Specifically, bidding games, and in particular bidding games of infinite duration, have an intriguing equivalence with random-turn games in which in each turn, the player who moves is chosen randomly. We show how minor changes in the bidding mechanism lead to unexpected differences in the equivalence with random-turn games.}, author = {Avni, Guy and Henzinger, Thomas A}, booktitle = {31st International Conference on Concurrency Theory}, isbn = {9783959771603}, issn = {18688969}, location = {Virtual}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{A survey of bidding games on graphs}}, doi = {10.4230/LIPIcs.CONCUR.2020.2}, volume = {171}, year = {2020}, } @inproceedings{8725, abstract = {The design and implementation of efficient concurrent data structures have seen significant attention. However, most of this work has focused on concurrent data structures providing good \emph{worst-case} guarantees. In real workloads, objects are often accessed at different rates, since access distributions may be non-uniform. Efficient distribution-adaptive data structures are known in the sequential case, e.g. the splay-trees; however, they often are hard to translate efficiently in the concurrent case. In this paper, we investigate distribution-adaptive concurrent data structures and propose a new design called the splay-list. At a high level, the splay-list is similar to a standard skip-list, with the key distinction that the height of each element adapts dynamically to its access rate: popular elements ``move up,'' whereas rarely-accessed elements decrease in height. We show that the splay-list provides order-optimal amortized complexity bounds for a subset of operations while being amenable to efficient concurrent implementation. Experimental results show that the splay-list can leverage distribution-adaptivity to improve on the performance of classic concurrent designs, and can outperform the only previously-known distribution-adaptive design in certain settings.}, author = {Aksenov, Vitaly and Alistarh, Dan-Adrian and Drozdova, Alexandra and Mohtashami, Amirkeivan}, booktitle = {34th International Symposium on Distributed Computing}, isbn = {9783959771689}, issn = {1868-8969}, location = {Freiburg, Germany}, pages = {3:1--3:18}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{The splay-list: A distribution-adaptive concurrent skip-list}}, doi = {10.4230/LIPIcs.DISC.2020.3}, volume = {179}, year = {2020}, } @article{8726, abstract = {Several realistic spin-orbital models for transition metal oxides go beyond the classical expectations and could be understood only by employing the quantum entanglement. Experiments on these materials confirm that spin-orbital entanglement has measurable consequences. Here, we capture the essential features of spin-orbital entanglement in complex quantum matter utilizing 1D spin-orbital model which accommodates SU(2)⊗SU(2) symmetric Kugel-Khomskii superexchange as well as the Ising on-site spin-orbit coupling. Building on the results obtained for full and effective models in the regime of strong spin-orbit coupling, we address the question whether the entanglement found on superexchange bonds always increases when the Ising spin-orbit coupling is added. We show that (i) quantum entanglement is amplified by strong spin-orbit coupling and, surprisingly, (ii) almost classical disentangled states are possible. We complete the latter case by analyzing how the entanglement existing for intermediate values of spin-orbit coupling can disappear for higher values of this coupling.}, author = {Gotfryd, Dorota and Paerschke, Ekaterina and Wohlfeld, Krzysztof and Oleś, Andrzej M.}, issn = {2410-3896}, journal = {Condensed Matter}, number = {3}, publisher = {MDPI}, title = {{Evolution of spin-orbital entanglement with increasing ising spin-orbit coupling}}, doi = {10.3390/condmat5030053}, volume = {5}, year = {2020}, } @inproceedings{9040, abstract = {Machine learning and formal methods have complimentary benefits and drawbacks. In this work, we address the controller-design problem with a combination of techniques from both fields. The use of black-box neural networks in deep reinforcement learning (deep RL) poses a challenge for such a combination. Instead of reasoning formally about the output of deep RL, which we call the wizard, we extract from it a decision-tree based model, which we refer to as the magic book. Using the extracted model as an intermediary, we are able to handle problems that are infeasible for either deep RL or formal methods by themselves. First, we suggest, for the first time, a synthesis procedure that is based on a magic book. We synthesize a stand-alone correct-by-design controller that enjoys the favorable performance of RL. Second, we incorporate a magic book in a bounded model checking (BMC) procedure. BMC allows us to find numerous traces of the plant under the control of the wizard, which a user can use to increase the trustworthiness of the wizard and direct further training.}, author = {Alamdari, Par Alizadeh and Avni, Guy and Henzinger, Thomas A and Lukina, Anna}, booktitle = {Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design}, isbn = {9783854480426}, issn = {2708-7824}, location = {Online Conference}, pages = {138--147}, publisher = {TU Wien Academic Press}, title = {{Formal methods with a touch of magic}}, doi = {10.34727/2020/isbn.978-3-85448-042-6_21}, year = {2020}, }