134 Works

Algorithms for Game Metrics

Krishnendu Chatterjee, Luca De Alfaro, Rupak Majumdar & Vishwanath Raman
Simulation and bisimulation metrics for stochastic systems provide a quantitative generalization of the classical simulation and bisimulation relations. These metrics capture the similarity of states with respect to quantitative specifications written in the quantitative $\mu$-calculus and related probabilistic logics. We present algorithms for computing the metrics on Markov decision processes (MDPs), turn-based stochastic games, and concurrent games. For turn-based games and MDPs, we provide a polynomial-time algorithm based on linear programming for the computation of...

Boolean algebras of unambiguous context-free languages

Didier Caucal
Several recent works have studied subfamilies of deterministic context-free languages with good closure properties, for instance the families of input-driven or visibly pushdown languages, or more generally families of languages accepted by pushdown automata whose stack height can be uniquely determined by the input word read so far. These ideas can be described as a notion of synchronization. In this paper we present an extension of synchronization to all context-free languages using graph grammars. This...

Increasing the power of the verifier in Quantum Zero Knowledge

Andre Chailloux & Iordanis Kerenidis
In quantum zero knowledge, the assumption was made that the verifier is only using unitary operations. Under this assumption, many nice properties have been shown about quantum zero knowledge, including the fact that Honest-Verifier Quantum Statistical Zero Knowledge ($HVQSZK$) is equal to Cheating-Verifier Quantum Statistical Zero Knowledge ($QSZK$) (see ~\cite{Wat02,Wat06}). In this paper, we study what happens when we allow an honest verifier to flip some coins in addition to using unitary operations. Flipping a...

Analyzing Asynchronous Programs with Preemption

Mohamed Faouzi Atig, Ahmed Bouajjani & Tayssir Touili
Multiset pushdown systems have been introduced by Sen and Viswanathan as an adequate model for asynchronous programs where some procedure calls can be stored as tasks to be processed later. The model is a pushdown system supplied with a multiset of pending tasks. Tasks may be added to the multiset at each transition, whereas a task is taken from the multiset only when the stack is empty. In this paper, we consider an extension of...

Some Sieving Algorithms for Lattice Problems

V. Arvind & Pushkar S. Joglekar
We study the algorithmic complexity of lattice problems based on the sieving technique due to Ajtai, Kumar, and Sivakumar~\cite{aks}. Given a $k$-dimensional subspace $M\subseteq \R^n$ and a full rank integer lattice $\L\subseteq \Q^n$, the \emph{subspace avoiding problem} SAP, defined by Bl\"omer and Naewe \cite{blomer}, is to find a shortest vector in $\L\setminus M$. We first give a $2^{O(n+k \log k)}$ time algorithm to solve \emph{the subspace avoiding problem}. Applying this algorithm we obtain the following...

Sound Lemma Generation for Proving Inductive Validity of Equations

Takahito Aoto
In many automated methods for proving inductive theorems, finding a suitable generalization of a conjecture is a key for the success of proof attempts. On the other hand, an obtained generalized conjecture may not be a theorem, and in this case hopeless proof attempts for the incorrect conjecture are made, which is against the success and efficiency of theorem proving. Urso and Kounalis (2004) proposed a generalization method for proving inductive validity of equations, called...

Runtime Monitoring of Metric First-order Temporal Properties

David Basin, Felix Klaedtke, Samuel Müller & Birgit Pfitzmann
We introduce a novel approach to the runtime monitoring of complex system properties. In particular, we present an online algorithm for a safety fragment of metric first-order temporal logic that is considerably more expressive than the logics supported by prior monitoring methods. Our approach, based on automatic structures, allows the unrestricted use of negation, universal and existential quantification over infinite domains, and the arbitrary nesting of both past and bounded future operators. Moreover, we show...

Solvency Games

Noam Berger, Nevin Kapur, Leonard Schulman & Vijay Vazirani
We study the decision theory of a maximally risk-averse investor --- one whose objective, in the face of stochastic uncertainties, is to minimize the probability of ever going broke. With a view to developing the mathematical basics of such a theory, we start with a very simple model and obtain the following results: a characterization of best play by investors; an explanation of why poor and rich players may have different best strategies; an explanation...

Implicit Branching and Parameterized Partial Cover Problems (Extended Abstract)

Omid Amini, Fedor Fomin & Saket Saurabh
Covering problems are fundamental classical problems in optimization, computer science and complexity theory. Typically an input to these problems is a family of sets over a finite universe and the goal is to cover the elements of the universe with as few sets of the family as possible. The variations of covering problems include well known problems like Set Cover, Vertex Cover, Dominating Set and Facility Location to name a few. Recently there has been...

Registration Year

  • 2009
    134

Resource Types

  • Text
    134

Data Centers

  • Dagstuhl
    134