@inproceedings{1068,
abstract = {Games on graphs provide the appropriate framework to study several central problems in computer science, such as verification and synthesis of reactive systems. One of the most basic objectives for games on graphs is the liveness (or Büchi) objective that given a target set of vertices requires that some vertex in the target set is visited infinitely often. We study generalized Büchi objectives (i.e., conjunction of liveness objectives), and implications between two generalized Büchi objectives (known as GR(1) objectives), that arise in numerous applications in computer-aided verification. We present improved algorithms and conditional super-linear lower bounds based on widely believed assumptions about the complexity of (A1) combinatorial Boolean matrix multiplication and (A2) CNF-SAT. We consider graph games with n vertices, m edges, and generalized Büchi objectives with k conjunctions. First, we present an algorithm with running time O(k*n^2), improving the previously known O(k*n*m) and O(k^2*n^2) worst-case bounds. Our algorithm is optimal for dense graphs under (A1). Second, we show that the basic algorithm for the problem is optimal for sparse graphs when the target sets have constant size under (A2). Finally, we consider GR(1) objectives, with k_1 conjunctions in the antecedent and k_2 conjunctions in the consequent, and present an O(k_1 k_2 n^{2.5})-time algorithm, improving the previously known O(k_1*k_2*n*m)-time algorithm for m > n^{1.5}. },
author = {Chatterjee, Krishnendu and Dvorák, Wolfgang and Henzinger, Monika and Loitzenbauer, Veronika},
location = {Krakow, Poland},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{Conditionally optimal algorithms for generalized Büchi Games}},
doi = {10.4230/LIPIcs.MFCS.2016.25},
volume = {58},
year = {2016},
}
@inproceedings{1069,
abstract = {The Continuous Skolem Problem asks whether a real-valued function satisfying a linear differen-
tial equation has a zero in a given interval of real numbers. This is a fundamental reachability
problem for continuous linear dynamical systems, such as linear hybrid automata and continuous-
time Markov chains. Decidability of the problem is currently open – indeed decidability is open
even for the sub-problem in which a zero is sought in a bounded interval. In this paper we show
decidability of the bounded problem subject to Schanuel’s Conjecture, a unifying conjecture in
transcendental number theory. We furthermore analyse the unbounded problem in terms of the
frequencies of the differential equation, that is, the imaginary parts of the characteristic roots.
We show that the unbounded problem can be reduced to the bounded problem if there is at most
one rationally linearly independent frequency, or if there are two rationally linearly independent
frequencies and all characteristic roots are simple. We complete the picture by showing that de-
cidability of the unbounded problem in the case of two (or more) rationally linearly independent
frequencies would entail a major new effectiveness result in Diophantine approximation, namely
computability of the Diophantine-approximation types of all real algebraic numbers.},
author = {Chonev, Ventsislav K and Ouaknine, Joël and Worrell, James},
location = {Rome, Italy},
publisher = {Schloss Dagstuhl- Leibniz-Zentrum fur Informatik},
title = {{On the skolem problem for continuous linear dynamical systems}},
doi = {10.4230/LIPIcs.ICALP.2016.100},
volume = {55},
year = {2016},
}
@inproceedings{1070,
abstract = {We present a logic that extends CTL (Computation Tree Logic) with operators that express synchronization properties. A property is synchronized in a system if it holds in all paths of a certain length. The new logic is obtained by using the same path quantifiers and temporal operators as in CTL, but allowing a different order of the quantifiers. This small syntactic variation induces a logic that can express non-regular properties for which known extensions of MSO with equality of path length are undecidable. We show that our variant of CTL is decidable and that the model-checking problem is in Delta_3^P = P^{NP^NP}, and is DP-hard. We analogously consider quantifier exchange in extensions of CTL, and we present operators defined using basic operators of CTL* that express the occurrence of infinitely many synchronization points. We show that the model-checking problem remains in Delta_3^P. The distinguishing power of CTL and of our new logic coincide if the Next operator is allowed in the logics, thus the classical bisimulation quotient can be used for state-space reduction before model checking. },
author = {Chatterjee, Krishnendu and Doyen, Laurent},
location = {Rome, Italy},
publisher = {Schloss Dagstuhl- Leibniz-Zentrum fur Informatik},
title = {{Computation tree logic for synchronization properties}},
doi = {10.4230/LIPIcs.ICALP.2016.98},
volume = {55},
year = {2016},
}
@inproceedings{1071,
abstract = {We consider data-structures for answering reachability and distance queries on constant-treewidth graphs with n nodes, on the standard RAM computational model with wordsize W=Theta(log n). Our first contribution is a data-structure that after O(n) preprocessing time, allows (1) pair reachability queries in O(1) time; and (2) single-source reachability queries in O(n/log n) time. This is (asymptotically) optimal and is faster than DFS/BFS when answering more than a constant number of single-source queries. The data-structure uses at all times O(n) space. Our second contribution is a space-time tradeoff data-structure for distance queries. For any epsilon in [1/2,1], we provide a data-structure with polynomial preprocessing time that allows pair queries in O(n^{1-\epsilon} alpha(n)) time, where alpha is the inverse of the Ackermann function, and at all times uses O(n^epsilon) space. The input graph G is not considered in the space complexity. },
author = {Chatterjee, Krishnendu and Ibsen-Jensen, Rasmus and Pavlogiannis, Andreas},
location = {Aarhus, Denmark},
publisher = {Schloss Dagstuhl- Leibniz-Zentrum fur Informatik},
title = {{Optimal reachability and a space time tradeoff for distance queries in constant treewidth graphs}},
doi = {10.4230/LIPIcs.ESA.2016.28},
volume = {57},
year = {2016},
}
@inproceedings{1090,
abstract = { While weighted automata provide a natural framework to express quantitative properties, many basic properties like average response time cannot be expressed with weighted automata. Nested weighted automata extend weighted automata and consist of a master automaton and a set of slave automata that are invoked by the master automaton. Nested weighted automata are strictly more expressive than weighted automata (e.g., average response time can be expressed with nested weighted automata), but the basic decision questions have higher complexity (e.g., for deterministic automata, the emptiness question for nested weighted automata is PSPACE-hard, whereas the corresponding complexity for weighted automata is PTIME). We consider a natural subclass of nested weighted automata where at any point at most a bounded number k of slave automata can be active. We focus on automata whose master value function is the limit average. We show that these nested weighted automata with bounded width are strictly more expressive than weighted automata (e.g., average response time with no overlapping requests can be expressed with bound k=1, but not with non-nested weighted automata). We show that the complexity of the basic decision problems (i.e., emptiness and universality) for the subclass with k constant matches the complexity for weighted automata. Moreover, when k is part of the input given in unary we establish PSPACE-completeness.},
author = {Chatterjee, Krishnendu and Henzinger, Thomas A and Otop, Jan},
location = {Krakow; Poland},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{Nested weighted limit-average automata of bounded width}},
doi = {10.4230/LIPIcs.MFCS.2016.24},
volume = {58},
year = {2016},
}
@inproceedings{1093,
abstract = {We introduce a general class of distances (metrics) between Markov chains, which are based on linear behaviour. This class encompasses distances given topologically (such as the total variation distance or trace distance) as well as by temporal logics or automata. We investigate which of the distances can be approximated by observing the systems, i.e. by black-box testing or simulation, and we provide both negative and positive results. },
author = {Daca, Przemyslaw and Henzinger, Thomas A and Kretinsky, Jan and Petrov, Tatjana},
location = {Quebec City; Canada},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{Linear distances between Markov chains}},
doi = {10.4230/LIPIcs.CONCUR.2016.20},
volume = {59},
year = {2016},
}
@inproceedings{1138,
abstract = {Automata with monitor counters, where the transitions do not depend on counter values, and nested weighted automata are two expressive automata-theoretic frameworks for quantitative properties. For a well-studied and wide class of quantitative functions, we establish that automata with monitor counters and nested weighted automata are equivalent. We study for the first time such quantitative automata under probabilistic semantics. We show that several problems that are undecidable for the classical questions of emptiness and universality become decidable under the probabilistic semantics. We present a complete picture of decidability for such automata, and even an almost-complete picture of computational complexity, for the probabilistic questions we consider. © 2016 ACM.},
author = {Chatterjee, Krishnendu and Henzinger, Thomas A and Otop, Jan},
booktitle = {Proceedings of the 31st Annual ACM/IEEE Symposium},
location = {New York, NY, USA},
pages = {76 -- 85},
publisher = {IEEE},
title = {{Quantitative automata under probabilistic semantics}},
doi = {10.1145/2933575.2933588},
year = {2016},
}
@inproceedings{1140,
abstract = {Given a model of a system and an objective, the model-checking question asks whether the model satisfies the objective. We study polynomial-time problems in two classical models, graphs and Markov Decision Processes (MDPs), with respect to several fundamental -regular objectives, e.g., Rabin and Streett objectives. For many of these problems the best-known upper bounds are quadratic or cubic, yet no super-linear lower bounds are known. In this work our contributions are two-fold: First, we present several improved algorithms, and second, we present the first conditional super-linear lower bounds based on widely believed assumptions about the complexity of CNF-SAT and combinatorial Boolean matrix multiplication. A separation result for two models with respect to an objective means a conditional lower bound for one model that is strictly higher than the existing upper bound for the other model, and similarly for two objectives with respect to a model. Our results establish the following separation results: (1) A separation of models (graphs and MDPs) for disjunctive queries of reachability and Büchi objectives. (2) Two kinds of separations of objectives, both for graphs and MDPs, namely, (2a) the separation of dual objectives such as Streett/Rabin objectives, and (2b) the separation of conjunction and disjunction of multiple objectives of the same type such as safety, Büchi, and coBüchi. In summary, our results establish the first model and objective separation results for graphs and MDPs for various classical -regular objectives. Quite strikingly, we establish conditional lower bounds for the disjunction of objectives that are strictly higher than the existing upper bounds for the conjunction of the same objectives. © 2016 ACM.},
author = {Chatterjee, Krishnendu and Dvoák, Wolfgang and Henzinger, Monika and Loitzenbauer, Veronika},
booktitle = {Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science},
location = {New York, NY, USA},
pages = {197 -- 206},
publisher = {IEEE},
title = {{Model and objective separation with conditional lower bounds disjunction is harder than conjunction}},
doi = {10.1145/2933575.2935304},
year = {2016},
}
@inproceedings{1166,
abstract = {POMDPs are standard models for probabilistic planning problems, where an agent interacts with an uncertain environment. We study the problem of almost-sure reachability, where given a set of target states, the question is to decide whether there is a policy to ensure that the target set is reached with probability 1 (almost-surely). While in general the problem is EXPTIMEcomplete, in many practical cases policies with a small amount of memory suffice. Moreover, the existing solution to the problem is explicit, which first requires to construct explicitly an exponential reduction to a belief-support MDP. In this work, we first study the existence of observation-stationary strategies, which is NP-complete, and then small-memory strategies. We present a symbolic algorithm by an efficient encoding to SAT and using a SAT solver for the problem. We report experimental results demonstrating the scalability of our symbolic (SAT-based) approach. © 2016, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.},
author = {Chatterjee, Krishnendu and Chmelik, Martin and Davies, Jessica},
booktitle = {Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence},
location = {Phoenix, AZ, USA},
pages = {3225 -- 3232},
publisher = {AAAI Press},
title = {{A symbolic SAT based algorithm for almost sure reachability with small strategies in pomdps}},
volume = {2016},
year = {2016},
}
@inproceedings{1182,
abstract = {Balanced knockout tournaments are ubiquitous in sports competitions and are also used in decisionmaking and elections. The traditional computational question, that asks to compute a draw (optimal draw) that maximizes the winning probability for a distinguished player, has received a lot of attention. Previous works consider the problem where the pairwise winning probabilities are known precisely, while we study how robust is the winning probability with respect to small errors in the pairwise winning probabilities. First, we present several illuminating examples to establish: (a) there exist deterministic tournaments (where the pairwise winning probabilities are 0 or 1) where one optimal draw is much more robust than the other; and (b) in general, there exist tournaments with slightly suboptimal draws that are more robust than all the optimal draws. The above examples motivate the study of the computational problem of robust draws that guarantee a specified winning probability. Second, we present a polynomial-time algorithm for approximating the robustness of a draw for sufficiently small errors in pairwise winning probabilities, and obtain that the stated computational problem is NP-complete. We also show that two natural cases of deterministic tournaments where the optimal draw could be computed in polynomial time also admit polynomial-time algorithms to compute robust optimal draws.},
author = {Chatterjee, Krishnendu and Ibsen-Jensen, Rasmus and Tkadlec, Josef},
location = {New York, NY, USA},
pages = {172 -- 179},
publisher = {AAAI Press},
title = {{Robust draws in balanced knockout tournaments}},
volume = {2016-January},
year = {2016},
}