@techreport{5401,
abstract = {This document is created as a part of the project “Repository for Research Data at IST Austria”. It summarises the actual initiatives, projects and standards related to the project. It supports the preparation of standards and specifications for the project, which should be considered and followed to ensure interoperability and visibility of the uploaded data.},
author = {Porsche, Jana},
publisher = {IST Austria},
title = {{Initiatives and projects related to RD}},
year = {2013},
}
@misc{5402,
abstract = {Linearizability requires that the outcome of calls by competing threads to a concurrent data structure is the same as some sequential execution where each thread has exclusive access to the data structure. In an ordered data structure, such as a queue or a stack, linearizability is ensured by requiring threads commit in the order dictated by the sequential semantics of the data structure; e.g., in a concurrent queue implementation a dequeue can only remove the oldest element.
In this paper, we investigate the impact of this strict ordering, by comparing what linearizability allows to what existing implementations do. We first give an operational definition for linearizability which allows us to build the most general linearizable implementation as a transition system for any given sequential specification. We then use this operational definition to categorize linearizable implementations based on whether they are bound or free. In a bound implementation, whenever all threads observe the same logical state, the updates to the logical state and the temporal order of commits coincide. All existing queue implementations we know of are bound. We then proceed to present, to the best of our knowledge, the first ever free queue implementation. Our experiments show that free implementations have the potential for better performance by suffering less from contention.},
author = {Henzinger, Thomas A and Sezgin, Ali},
issn = {2664-1690},
pages = {16},
publisher = {IST Austria},
title = {{How free is your linearizable concurrent data structure?}},
doi = {10.15479/AT:IST-2013-123-v1-1},
year = {2013},
}
@misc{5403,
abstract = {We consider concurrent games played by two-players on a finite state graph, where in every round the players simultaneously choose a move, and the current state along with the joint moves determine the successor state. We study the most fundamental objective for concurrent games, namely, mean-payoff or limit-average objective, where a reward is associated to every transition, and the goal of player 1 is to maximize the long-run average of the rewards, and the objective of player 2 is strictly the opposite (i.e., the games are zero-sum). The path constraint for player 1 could be qualitative, i.e., the mean-payoff is the maximal reward, or arbitrarily close to it; or quantitative, i.e., a given threshold between the minimal and maximal reward. We consider the computation of the almost-sure (resp. positive) winning sets, where player 1 can ensure that the path constraint is satisfied with probability 1 (resp. positive probability). Almost-sure winning with qualitative constraint exactly corresponds to the question whether there exists a strategy to ensure that the payoff is the maximal reward of the game. Our main results for qualitative path constraints are as follows: (1) we establish qualitative determinacy results that show for every state either player 1 has a strategy to ensure almost-sure (resp. positive) winning against all player-2 strategies or player 2 has a spoiling strategy to falsify almost-sure (resp. positive) winning against all player-1 strategies; (2) we present optimal strategy complexity results that precisely characterize the classes of strategies required for almost-sure and positive winning for both players; and (3) we present quadratic time algorithms to compute the almost-sure and the positive winning sets, matching the best known bound of the algorithms for much simpler problems (such as reachability objectives). For quantitative constraints we show that a polynomial time solution for the almost-sure or the positive winning set would imply a solution to a long-standing open problem (of solving the value problem of mean-payoff games) that is not known to be in polynomial time.},
author = {Chatterjee, Krishnendu and Ibsen-Jensen, Rasmus},
issn = {2664-1690},
pages = {33},
publisher = {IST Austria},
title = {{Qualitative analysis of concurrent mean-payoff games}},
doi = {10.15479/AT:IST-2013-126-v1-1},
year = {2013},
}
@misc{5404,
abstract = {We study finite-state two-player (zero-sum) concurrent mean-payoff games played on a graph. We focus on the important sub-class of ergodic games where all states are visited infinitely often with probability 1. The algorithmic study of ergodic games was initiated in a seminal work of Hoffman and Karp in 1966, but all basic complexity questions have remained unresolved. Our main results for ergodic games are as follows: We establish (1) an optimal exponential bound on the patience of stationary strategies (where patience of a distribution is the inverse of the smallest positive probability and represents a complexity measure of a stationary strategy); (2) the approximation problem lie in FNP; (3) the approximation problem is at least as hard as the decision problem for simple stochastic games (for which NP and coNP is the long-standing best known bound). We show that the exact value can be expressed in the existential theory of the reals, and also establish square-root sum hardness for a related class of games.},
author = {Chatterjee, Krishnendu and Ibsen-Jensen, Rasmus},
issn = {2664-1690},
pages = {29},
publisher = {IST Austria},
title = {{The complexity of ergodic games}},
doi = {10.15479/AT:IST-2013-127-v1-1},
year = {2013},
}
@misc{5405,
abstract = {The theory of graph games is the foundation for modeling and synthesizing reactive processes. In the synthesis of stochastic processes, we use 2-1/2-player games where some transitions of the game graph are controlled by two adversarial players, the System and the Environment, and the other transitions are determined probabilistically. We consider 2-1/2-player games where the objective of the System is the conjunction of a qualitative objective (specified as a parity condition) and a quantitative objective (specified as a mean-payoff condition). We establish that the problem of deciding whether the System can ensure that the probability to satisfy the mean-payoff parity objective is at least a given threshold is in NP ∩ coNP, matching the best known bound in the special case of 2-player games (where all transitions are deterministic) with only parity objectives, or with only mean-payoff objectives. We present an algorithm running
in time O(d · n^{2d}·MeanGame) to compute the set of almost-sure winning states from which the objective
can be ensured with probability 1, where n is the number of states of the game, d the number of priorities
of the parity objective, and MeanGame is the complexity to compute the set of almost-sure winning states
in 2-1/2-player mean-payoff games. Our results are useful in the synthesis of stochastic reactive systems
with both functional requirement (given as a qualitative objective) and performance requirement (given
as a quantitative objective).},
author = {Chatterjee, Krishnendu and Doyen, Laurent and Gimbert, Hugo and Oualhadj, Youssouf},
issn = {2664-1690},
pages = {22},
publisher = {IST Austria},
title = {{Perfect-information stochastic mean-payoff parity games}},
doi = {10.15479/AT:IST-2013-128-v1-1},
year = {2013},
}
@misc{5406,
abstract = {We consider the distributed synthesis problem fortemporal logic specifications. Traditionally, the problem has been studied for LTL, and the previous results show that the problem is decidable iff there is no information fork in the architecture. We consider the problem for fragments of LTLand our main results are as follows: (1) We show that the problem is undecidable for architectures with information forks even for the fragment of LTL with temporal operators restricted to next and eventually. (2) For specifications restricted to globally along with non-nested next operators, we establish decidability (in EXPSPACE) for star architectures where the processes receive disjoint inputs, whereas we establish undecidability for architectures containing an information fork-meet structure. (3)Finally, we consider LTL without the next operator, and establish decidability (NEXPTIME-complete) for all architectures for a fragment that consists of a set of safety assumptions, and a set of guarantees where each guarantee is a safety, reachability, or liveness condition.},
author = {Chatterjee, Krishnendu and Henzinger, Thomas A and Otop, Jan and Pavlogiannis, Andreas},
issn = {2664-1690},
pages = {11},
publisher = {IST Austria},
title = {{Distributed synthesis for LTL Fragments}},
doi = {10.15479/AT:IST-2013-130-v1-1},
year = {2013},
}
@techreport{5407,
abstract = {This document is created as a part of the project “Repository for Research Data at IST Austria”. It summarises the mandatory features, which need to be fulfilled to provide an institutional repository as a platform and also a service to the scientists at the institute. It also includes optional features, which would be of strong benefit for the scientists and would increase the usage of the repository, and hence the visibility of research at IST Austria.},
author = {Porsche, Jana},
publisher = {IST Austria},
title = {{Technical requirements and features}},
year = {2013},
}
@misc{5408,
abstract = {We consider two-player partial-observation stochastic games where player 1 has partial observation and player 2 has perfect observation. The winning condition we study are omega-regular conditions specified as parity objectives. The qualitative analysis problem given a partial-observation stochastic game and a parity objective asks whether there is a strategy to ensure that the objective is satisfied with probability 1 (resp. positive probability). While the qualitative analysis problems are known to be undecidable even for very special cases of parity objectives, they were shown to be decidable in 2EXPTIME under finite-memory strategies. We improve the complexity and show that the qualitative analysis problems for partial-observation stochastic parity games under finite-memory strategies are
EXPTIME-complete; and also establish optimal (exponential) memory bounds for finite-memory strategies required for qualitative analysis. },
author = {Chatterjee, Krishnendu and Doyen, Laurent and Nain, Sumit and Vardi, Moshe},
issn = {2664-1690},
pages = {17},
publisher = {IST Austria},
title = {{The complexity of partial-observation stochastic parity games with finite-memory strategies}},
doi = {10.15479/AT:IST-2013-141-v1-1},
year = {2013},
}
@misc{5409,
abstract = {The edit distance between two (untimed) traces is the minimum cost of a sequence of edit operations (insertion, deletion, or substitution) needed to transform one trace to the other. Edit distances have been extensively studied in the untimed setting, and form the basis for approximate matching of sequences in different domains such as coding theory, parsing, and speech recognition.
In this paper, we lift the study of edit distances from untimed languages to the timed setting. We define an edit distance between timed words which incorporates both the edit distance between the untimed words and the absolute difference in timestamps. Our edit distance between two timed words is computable in polynomial time. Further, we show that the edit distance between a timed word and a timed language generated by a timed automaton, defined as the edit distance between the word and the closest word in the language, is PSPACE-complete. While computing the edit distance between two timed automata is undecidable, we show that the approximate version, where we decide if the edit distance between two timed automata is either less than a given parameter or more than delta away from the parameter, for delta>0, can be solved in exponential space and is EXPSPACE-hard. Our definitions and techniques can be generalized to the setting of hybrid systems, and we show analogous decidability results for rectangular automata.},
author = {Chatterjee, Krishnendu and Ibsen-Jensen, Rasmus and Majumdar, Rupak},
issn = {2664-1690},
pages = {12},
publisher = {IST Austria},
title = {{Edit distance for timed automata}},
doi = {10.15479/AT:IST-2013-144-v1-1},
year = {2013},
}
@misc{5410,
abstract = {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.
Our 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. },
author = {Ahmed, Umair and Chatterjee, Krishnendu and Gulwani, Sumit},
issn = {2664-1690},
pages = {13},
publisher = {IST Austria},
title = {{Automatic generation of alternative starting positions for traditional board games}},
doi = {10.15479/AT:IST-2013-146-v1-1},
year = {2013},
}
@inbook{5747,
author = {Dragoi, Cezara and Gupta, Ashutosh and Henzinger, Thomas A},
booktitle = {Computer Aided Verification},
isbn = {9783642397981},
issn = {0302-9743},
location = {Saint Petersburg, Russia},
pages = {174--190},
publisher = {Springer Berlin Heidelberg},
title = {{Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates}},
doi = {10.1007/978-3-642-39799-8_11},
volume = {8044},
year = {2013},
}
@misc{6440,
abstract = {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.},
author = {Henzinger, Thomas A and Payer, Hannes and Sezgin, Ali},
issn = {2664-1690},
pages = {23},
publisher = {IST Austria},
title = {{Replacing competition with cooperation to achieve scalable lock-free FIFO queues }},
doi = {10.15479/AT:IST-2013-124-v1-1},
year = {2013},
}
@inproceedings{1374,
abstract = {We study two-player zero-sum games over infinite-state graphs equipped with ωB and finitary conditions. Our first contribution is about the strategy complexity, i.e the memory required for winning strategies: we prove that over general infinite-state graphs, memoryless strategies are sufficient for finitary Büchi, and finite-memory suffices for finitary parity games. We then study pushdown games with boundedness conditions, with two contributions. First we prove a collapse result for pushdown games with ωB-conditions, implying the decidability of solving these games. Second we consider pushdown games with finitary parity along with stack boundedness conditions, and show that solving these games is EXPTIME-complete.},
author = {Chatterjee, Krishnendu and Fijalkow, Nathanaël},
booktitle = {22nd EACSL Annual Conference on Computer Science Logic},
location = {Torino, Italy},
pages = {181 -- 196},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{Infinite-state games with finitary conditions}},
doi = {10.4230/LIPIcs.CSL.2013.181},
volume = {23},
year = {2013},
}
@inproceedings{1385,
abstract = {It is often difficult to correctly implement a Boolean controller for a complex system, especially when concurrency is involved. Yet, it may be easy to formally specify a controller. For instance, for a pipelined processor it suffices to state that the visible behavior of the pipelined system should be identical to a non-pipelined reference system (Burch-Dill paradigm). We present a novel procedure to efficiently synthesize multiple Boolean control signals from a specification given as a quantified first-order formula (with a specific quantifier structure). Our approach uses uninterpreted functions to abstract details of the design. We construct an unsatisfiable SMT formula from the given specification. Then, from just one proof of unsatisfiability, we use a variant of Craig interpolation to compute multiple coordinated interpolants that implement the Boolean control signals. Our method avoids iterative learning and back-substitution of the control functions. We applied our approach to synthesize a controller for a simple two-stage pipelined processor, and present first experimental results.},
author = {Hofferek, Georg and Gupta, Ashutosh and Könighofer, Bettina and Jiang, Jie and Bloem, Roderick},
booktitle = {2013 Formal Methods in Computer-Aided Design},
location = {Portland, OR, United States},
pages = {77 -- 84},
publisher = {IEEE},
title = {{Synthesizing multiple boolean functions using interpolation on a single proof}},
doi = {10.1109/FMCAD.2013.6679394},
year = {2013},
}
@inproceedings{1387,
abstract = {Choices made by nondeterministic word automata depend on both the past (the prefix of the word read so far) and the future (the suffix yet to be read). In several applications, most notably synthesis, the future is diverse or unknown, leading to algorithms that are based on deterministic automata. Hoping to retain some of the advantages of nondeterministic automata, researchers have studied restricted classes of nondeterministic automata. Three such classes are nondeterministic automata that are good for trees (GFT; i.e., ones that can be expanded to tree automata accepting the derived tree languages, thus whose choices should satisfy diverse futures), good for games (GFG; i.e., ones whose choices depend only on the past), and determinizable by pruning (DBP; i.e., ones that embody equivalent deterministic automata). The theoretical properties and relative merits of the different classes are still open, having vagueness on whether they really differ from deterministic automata. In particular, while DBP ⊆ GFG ⊆ GFT, it is not known whether every GFT automaton is GFG and whether every GFG automaton is DBP. Also open is the possible succinctness of GFG and GFT automata compared to deterministic automata. We study these problems for ω-regular automata with all common acceptance conditions. We show that GFT=GFG⊃DBP, and describe a determinization construction for GFG automata.},
author = {Boker, Udi and Kuperberg, Denis and Kupferman, Orna and Skrzypczak, Michał},
location = {Riga, Latvia},
number = {PART 2},
pages = {89 -- 100},
publisher = {Springer},
title = {{Nondeterminism in the presence of a diverse or unknown future}},
doi = {10.1007/978-3-642-39212-2_11},
volume = {7966},
year = {2013},
}
@article{450,
abstract = {Understanding the relative importance of heterosis and outbreeding depression over multiple generations is a key question in evolutionary biology and is essential for identifying appropriate genetic sources for population and ecosystem restoration. Here we use 2455 experimental crosses between 12 population pairs of the rare perennial plant Rutidosis leptorrhynchoides (Asteraceae) to investigate the multi-generational (F1, F2, F3) fitness outcomes of inter-population hybridization. We detected no evidence of outbreeding depression, with inter-population hybrids and backcrosses showing either similar fitness or significant heterosis for fitness components across the three generations. Variation in heterosis among population pairs was best explained by characteristics of the foreign source or home population, and was greatest when the source population was large, with high genetic diversity and low inbreeding, and the home population was small and inbred. Our results indicate that the primary consideration for maximizing progeny fitness following population augmentation or restoration is the use of seed from large, genetically diverse populations.},
author = {Pickup, Melinda and Field, David and Rowell, David and Young, Andrew},
journal = {Proceedings of the Royal Society of London Series B Biological Sciences},
number = {1750},
publisher = {Royal Society, The},
title = {{Source population characteristics affect heterosis following genetic rescue of fragmented plant populations}},
doi = {10.1098/rspb.2012.2058},
volume = {280},
year = {2013},
}
@article{3261,
abstract = {Cells in a developing embryo have no direct way of "measuring" their physical position. Through a variety of processes, however, the expression levels of multiple genes come to be correlated with position, and these expression levels thus form a code for "positional information." We show how to measure this information, in bits, using the gap genes in the Drosophila embryo as an example. Individual genes carry nearly two bits of information, twice as much as expected if the expression patterns consisted only of on/off domains separated by sharp boundaries. Taken together, four gap genes carry enough information to define a cell's location with an error bar of ~1% along the anterior-posterior axis of the embryo. This precision is nearly enough for each cell to have a unique identity, which is the maximum information the system can use, and is nearly constant along the length of the embryo. We argue that this constancy is a signature of optimality in the transmission of information from primary morphogen inputs to the output of the gap gene network.},
author = {Dubuis, Julien and Tkacik, Gasper and Wieschaus, Eric and Gregor, Thomas and Bialek, William},
journal = {PNAS},
number = {41},
pages = {16301 -- 16308},
publisher = {National Academy of Sciences},
title = {{Positional information, in bits}},
doi = {10.1073/pnas.1315642110},
volume = {110},
year = {2013},
}
@phdthesis{1405,
abstract = {Motivated by the analysis of highly dynamic message-passing systems, i.e. unbounded thread creation, mobility, etc. we present a framework for the analysis of depth-bounded systems. Depth-bounded systems are one of the most expressive known fragment of the π-calculus for which interesting verification problems are still decidable. Even though they are infinite state systems depth-bounded systems are well-structured, thus can be analyzed algorithmically. We give an interpretation of depth-bounded systems as graph-rewriting systems. This gives more flexibility and ease of use to apply depth-bounded systems to other type of systems like shared memory concurrency.
First, we develop an adequate domain of limits for depth-bounded systems, a prerequisite for the effective representation of downward-closed sets. Downward-closed sets are needed by forward saturation-based algorithms to represent potentially infinite sets of states. Then, we present an abstract interpretation framework to compute the covering set of well-structured transition systems. Because, in general, the covering set is not computable, our abstraction over-approximates the actual covering set. Our abstraction captures the essence of acceleration based-algorithms while giving up enough precision to ensure convergence. We have implemented the analysis in the PICASSO tool and show that it is accurate in practice. Finally, we build some further analyses like termination using the covering set as starting point.},
author = {Zufferey, Damien},
pages = {134},
publisher = {IST Austria},
title = {{Analysis of dynamic message passing programs}},
year = {2013},
}
@inproceedings{2847,
abstract = {Depth-Bounded Systems form an expressive class of well-structured transition systems. They can model a wide range of concurrent infinite-state systems including those with dynamic thread creation, dynamically changing communication topology, and complex shared heap structures. We present the first method to automatically prove fair termination of depth-bounded systems. Our method uses a numerical abstraction of the system, which we obtain by systematically augmenting an over-approximation of the system’s reachable states with a finite set of counters. This numerical abstraction can be analyzed with existing termination provers. What makes our approach unique is the way in which it exploits the well-structuredness of the analyzed system. We have implemented our work in a prototype tool and used it to automatically prove liveness properties of complex concurrent systems, including nonblocking algorithms such as Treiber’s stack and several distributed processes. Many of these examples are beyond the scope of termination analyses that are based on traditional counter abstractions.},
author = {Bansal, Kshitij and Koskinen, Eric and Wies, Thomas and Zufferey, Damien},
editor = {Piterman, Nir and Smolka, Scott},
location = {Rome, Italy},
pages = {62 -- 77},
publisher = {Springer},
title = {{Structural Counter Abstraction}},
doi = {10.1007/978-3-642-36742-7_5},
volume = {7795},
year = {2013},
}
@inproceedings{2445,
abstract = {We develop program synthesis techniques that can help programmers fix concurrency-related bugs. We make two new contributions to synthesis for concurrency, the first improving the efficiency of the synthesized code, and the second improving the efficiency of the synthesis procedure itself. The first contribution is to have the synthesis procedure explore a variety of (sequential) semantics-preserving program transformations. Classically, only one such transformation has been considered, namely, the insertion of synchronization primitives (such as locks). Based on common manual bug-fixing techniques used by Linux device-driver developers, we explore additional, more efficient transformations, such as the reordering of independent instructions. The second contribution is to speed up the counterexample-guided removal of concurrency bugs within the synthesis procedure by considering partial-order traces (instead of linear traces) as counterexamples. A partial-order error trace represents a set of linear (interleaved) traces of a concurrent program all of which lead to the same error. By eliminating a partial-order error trace, we eliminate in a single iteration of the synthesis procedure all linearizations of the partial-order trace. We evaluated our techniques on several simplified examples of real concurrency bugs that occurred in Linux device drivers.},
author = {Cerny, Pavol and Henzinger, Thomas A and Radhakrishna, Arjun and Ryzhyk, Leonid and Tarrach, Thorsten},
location = {St. Petersburg, Russia},
pages = {951 -- 967},
publisher = {Springer},
title = {{Efficient synthesis for concurrency by semantics-preserving transformations}},
doi = {10.1007/978-3-642-39799-8_68},
volume = {8044},
year = {2013},
}