Searcharxiv⌕ Search

arXiv subjects

Antonín Kučera

Publications and source records attributed to Antonín Kučera.

At least 37 records · Page 2Linked to original sources
arXiv2018

Synthesizing Efficient Solutions for Patrolling Problems in the Internet Environment

We propose an algorithm for constructing efficient patrolling strategies in the Internet environment, where the protected targets are nodes connected to the network and the patrollers are software agents capable of detecting/preventing undesirable activities on the nodes. The algorithm is based on a novel compositional principle designed for a special class of strategies, and it can quickly construct (sub)optimal solutions even if the number of targets reaches hundreds of millions.

cs.AI↗
arXiv2018

Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS

Vector Addition Systems with States (VASS) provide a well-known and fundamental model for the analysis of concurrent processes, parameterized systems, and are also used as abstract models of programs in resource bound analysis. In this paper we study the problem of obtaining asymptotic bounds on the termination time of a given VASS. In particular, we focus on the practically important case of obtaining polynomial bounds on termination time. Our main contributions are as follows: First, we present a polynomial-time algorithm for deciding whether a given VASS has a linear asymptotic complexity. We also show that if the complexity of a VASS is not linear, it is at least quadratic. Second, we classify VASS according to quantitative properties of their cycles. We show that certain singularities in these properties are the key reason for non-polynomial asymptotic complexity of VASS. In absence of singularities, we show that the asymptotic complexity is always polynomial and of the form $Θ(n^k)$, for some integer $k\leq d$, where $d$ is the dimension of the VASS. We present a polynomial-time algorithm computing the optimal $k$. For general VASS, the same algorithm, which is based on a complete technique for the construction of ranking functions in VASS, produces a valid lower bound, i.e., a $k$ such that the termination complexity is $Ω(n^k)$. Our results are based on new insights into the geometry of VASS dynamics, which hold the potential for further applicability to VASS analysis.

cs.LO↗
arXiv2017

Efficient Algorithms for Checking Fast Termination in VASS

Vector Addition Systems with States (VASS) consists of a finite state space equipped with d counters, where in each transition every counter is incremented, decremented, or left unchanged. VASS provide a fundamental model for analysis of concurrent processes, parametrized systems, and they are also used as abstract models for programs for bounds analysis. While termination is the basic liveness property that asks the qualitative question of whether a given model always terminates or not, the more general quantitative question asks for bounds on the number of steps to termination. In the realm of quantitative bounds a fundamental problem is to obtain asymptotic bounds on termination time. Large asymptotic bounds such as exponential or higher already suggest that either there is some error in modeling, or the model is not useful in practice. Hence we focus on polynomial asymptotic bounds for VASS. While some well-known approaches (e.g., lexicographic ranking functions) are neither sound nor complete with respect to polynomial bounds, other approaches only present sound methods for upper bounds. In this work our main contributions are as follows: First, for linear asymptotic bounds we present a sound and complete method for VASS, and moreover, our algorithm runs in polynomial time. Second, we classify VASS according the normals of the vectors of the cycles. We show that singularities in the normal are the key reason for asymptotic bounds such as exponential and non-elementary for VASS. In absence of singularities, we show that the asymptotic complexity bound is always polynomial and of the form $Θ(n^k)$, for some k $\leq$ d. We present an algorithm, with time complexity polynomial in the size of the VASS and exponential in dimension d, to compute the optimal k.

cs.LO↗
arXiv2017

Mean-Payoff Optimization in Continuous-Time Markov Chains with Parametric Alarms

Continuous-time Markov chains with alarms (ACTMCs) allow for alarm events that can be non-exponentially distributed. Within parametric ACTMCs, the parameters of alarm-event distributions are not given explicitly and can be subject of parameter synthesis. An algorithm solving the $\varepsilon$-optimal parameter synthesis problem for parametric ACTMCs with long-run average optimization objectives is presented. Our approach is based on reduction of the problem to finding long-run average optimal strategies in semi-Markov decision processes (semi-MDPs) and sufficient discretization of parameter (i.e., action) space. Since the set of actions in the discretized semi-MDP can be very large, a straightforward approach based on explicit action-space construction fails to solve even simple instances of the problem. The presented algorithm uses an enhanced policy iteration on symbolic representations of the action space. The soundness of the algorithm is established for parametric ACTMCs with alarm-event distributions satisfying four mild assumptions that are shown to hold for uniform, Dirac and Weibull distributions in particular, but are satisfied for many other distributions as well. An experimental implementation shows that the symbolic technique substantially improves the efficiency of the synthesis algorithm and allows to solve instances of realistic size.

cs.PF↗
arXiv2016

Optimizing the Expected Mean Payoff in Energy Markov Decision Processes

Energy Markov Decision Processes (EMDPs) are finite-state Markov decision processes where each transition is assigned an integer counter update and a rational payoff. An EMDP configuration is a pair s(n), where s is a control state and n is the current counter value. The configurations are changed by performing transitions in the standard way. We consider the problem of computing a safe strategy (i.e., a strategy that keeps the counter non-negative) which maximizes the expected mean payoff.

cs.LO↗
arXiv2016

Efficient Timeout Synthesis in Fixed-Delay CTMC Using Policy Iteration

We consider the fixed-delay synthesis problem for continuous-time Markov chains extended with fixed-delay transitions (fdCTMC). The goal is to synthesize concrete values of the fixed-delays (timeouts) that minimize the expected total cost incurred before reaching a given set of target states. The same problem has been considered and solved in previous works by computing an optimal policy in a certain discrete-time Markov decision process (MDP) with a huge number of actions that correspond to suitably discretized values of the timeouts. In this paper, we design a symbolic fixed-delay synthesis algorithm which avoids the explicit construction of large action spaces. Instead, the algorithm computes a small sets of "promising" candidate actions on demand. The candidate actions are selected by minimizing a certain objective function by computing its symbolic derivative and extracting a univariate polynomial whose roots are precisely the points where the derivative takes zero value. Since roots of high degree univariate polynomials can be isolated very efficiently using modern mathematical software, we achieve not only drastic memory savings but also speedup by three orders of magnitude compared to the previous methods.

cs.PF↗
arXiv2016

Stability in Graphs and Games

We study graphs and two-player games in which rewards are assigned to states, and the goal of the players is to satisfy or dissatisfy certain property of the generated outcome, given as a mean payoff property. Since the notion of mean-payoff does not reflect possible fluctuations from the mean-payoff along a run, we propose definitions and algorithms for capturing the stability of the system, and give algorithms for deciding if a given mean payoff and stability objective can be ensured in the system

cs.LO↗
arXiv2015

Strategy Synthesis in Adversarial Patrolling Games

Patrolling is one of the central problems in operational security. Formally, a patrolling problem is specified by a set $U$ of nodes (admissible defender's positions), a set $T \subseteq U$ of vulnerable targets, an admissible defender's moves over $U$, and a function which to every target assigns the time needed to complete an intrusion at it. The goal is to design an optimal strategy for a defender who is moving from node to node and aims at detecting possible intrusions at the targets. The goal of the attacker is to maximize the probability of a successful attack. We assume that the attacker is adversarial, i.e., he knows the strategy of the defender and can observe her moves. We prove that the defender has an optimal strategy for every patrolling problem. Further, we show that for every $\varepsilon$ > 0, there exists a finite-memory $\varepsilon$-optimal strategy for the defender constructible in exponential time, and we observe that such a strategy cannot be computed in polynomial time unless P=NP. Then we focus ourselves to unrestricted defender's moves. Here, a patrolling problem is fully determined by its signature, the number of targets of each attack length. We bound the maximal probability of successfully defended attacks. Then, we introduce a decomposition method which allows to split a given patrolling problem $G$ into smaller subproblems and construct a defender's strategy for $G$ by "composing" the strategies constructed for these subproblems. Finally, for patrolling problems with $T = U$ and a well-formed signature, we give an exact classification of all sufficiently connected environments where the defender can achieve the same value as in the fully connected uniform environment. This result is useful for designing "good" environments where the defender can act optimally.

cs.GT↗
arXiv2015

MultiGain: A controller synthesis tool for MDPs with multiple mean-payoff objectives

We present MultiGain, a tool to synthesize strategies for Markov decision processes (MDPs) with multiple mean-payoff objectives. Our models are described in PRISM, and our tool uses the existing interface and simulator of PRISM. Our tool extends PRISM by adding novel algorithms for multiple mean-payoff objectives, and also provides features such as (i)~generating strategies and exploring them for simulation, and checking them with respect to other properties; and (ii)~generating an approximate Pareto curve for two mean-payoff objectives. In addition, we present a new practical algorithm for the analysis of MDPs with multiple mean-payoff objectives under memoryless strategies.

cs.AI↗
arXiv2014

Demuth's path to randomness

Osvald Demuth (1936--1988) studied constructive analysis from the viewpoint of the Russian school of constructive mathematics. In the course of his work he introduced various notions of effective null set which, when phrased in classical language, yield a number of major algorithmic randomness notions. In addition, he proved several results connecting constructive analysis and randomness that were rediscovered only much later. In this paper, we trace the path that took Demuth from his constructivist roots to his deep and innovative work on the interactions between constructive analysis, algorithmic randomness, and computability theory. We will focus specifically on (i) Demuth's work on the differentiability of Markov computable functions and his study of constructive versions of the Denjoy alternative, (ii) Demuth's independent discovery of the main notions of algorithmic randomness, as well as the development of Demuth randomness, and (iii) the interactions of truth-table reducibility, algorithmic randomness, and semigenericity in Demuth's work.

math.LO↗
arXiv2014

Minimizing Running Costs in Consumption Systems

A standard approach to optimizing long-run running costs of discrete systems is based on minimizing the mean-payoff, i.e., the long-run average amount of resources ("energy") consumed per transition. However, this approach inherently assumes that the energy source has an unbounded capacity, which is not always realistic. For example, an autonomous robotic device has a battery of finite capacity that has to be recharged periodically, and the total amount of energy consumed between two successive charging cycles is bounded by the capacity. Hence, a controller minimizing the mean-payoff must obey this restriction. In this paper we study the controller synthesis problem for consumption systems with a finite battery capacity, where the task of the controller is to minimize the mean-payoff while preserving the functionality of the system encoded by a given linear-time property. We show that an optimal controller always exists, and it may either need only finite memory or require infinite memory (it is decidable in polynomial time which of the two cases holds). Further, we show how to compute an effective description of an optimal controller in polynomial time. Finally, we consider the limit values achievable by larger and larger battery capacity, show that these values are computable in polynomial time, and we also analyze the corresponding rate of convergence. To the best of our knowledge, these are the first results about optimizing the long-run running costs in systems with bounded energy stores.

eess.SY↗
arXiv2014

Markov Decision Processes with Multiple Long-run Average Objectives

We study Markov decision processes (MDPs) with multiple limit-average (or mean-payoff) functions. We consider two different objectives, namely, expectation and satisfaction objectives. Given an MDP with k limit-average functions, in the expectation objective the goal is to maximize the expected limit-average value, and in the satisfaction objective the goal is to maximize the probability of runs such that the limit-average value stays above a given vector. We show that under the expectation objective, in contrast to the case of one limit-average function, both randomization and memory are necessary for strategies even for epsilon-approximation, and that finite-memory randomized strategies are sufficient for achieving Pareto optimal values. Under the satisfaction objective, in contrast to the case of one limit-average function, infinite memory is necessary for strategies achieving a specific value (i.e. randomized finite-memory strategies are not sufficient), whereas memoryless randomized strategies are sufficient for epsilon-approximation, for all epsilon>0. We further prove that the decision problems for both expectation and satisfaction objectives can be solved in polynomial time and the trade-off curve (Pareto curve) can be epsilon-approximated in time polynomial in the size of the MDP and 1/epsilon, and exponential in the number of limit-average functions, for all epsilon>0. Our analysis also reveals flaws in previous work for MDPs with multiple mean-payoff functions under the expectation objective, corrects the flaws, and allows us to obtain improved results.

cs.GT↗
arXiv2014

Zero-Reachability in Probabilistic Multi-Counter Automata

We study the qualitative and quantitative zero-reachability problem in probabilistic multi-counter systems. We identify the undecidable variants of the problems, and then we concentrate on the remaining two cases. In the first case, when we are interested in the probability of all runs that visit zero in some counter, we show that the qualitative zero-reachability is decidable in time which is polynomial in the size of a given pMC and doubly exponential in the number of counters. Further, we show that the probability of all zero-reaching runs can be effectively approximated up to an arbitrarily small given error epsilon > 0 in time which is polynomial in log(epsilon), exponential in the size of a given pMC, and doubly exponential in the number of counters. In the second case, we are interested in the probability of all runs that visit zero in some counter different from the last counter. Here we show that the qualitative zero-reachability is decidable and SquareRootSum-hard, and the probability of all zero-reaching runs can be effectively approximated up to an arbitrarily small given error epsilon > 0 (these result applies to pMC satisfying a suitable technical condition that can be verified in polynomial time). The proof techniques invented in the second case allow to construct counterexamples for some classical results about ergodicity in stochastic Petri nets.

cs.FL↗
arXiv2013

Trading Performance for Stability in Markov Decision Processes

We study the complexity of central controller synthesis problems for finite-state Markov decision processes, where the objective is to optimize both the expected mean-payoff performance of the system and its stability. We argue that the basic theoretical notion of expressing the stability in terms of the variance of the mean-payoff (called global variance in our paper) is not always sufficient, since it ignores possible instabilities on respective runs. For this reason we propose alernative definitions of stability, which we call local and hybrid variance, and which express how rewards on each run deviate from the run's own mean-payoff and from the expected mean-payoff, respectively. We show that a strategy ensuring both the expected mean-payoff and the variance below given bounds requires randomization and memory, under all the above semantics of variance. We then look at the problem of determining whether there is a such a strategy. For the global variance, we show that the problem is in PSPACE, and that the answer can be approximated in pseudo-polynomial time. For the hybrid variance, the analogous decision problem is in NP, and a polynomial-time approximating algorithm also exists. For local variance, we show that the decision problem is in NP. Since the overall performance can be traded for stability (and vice versa), we also present algorithms for approximating the associated Pareto curve in all the three cases. Finally, we study a special case of the decision problems, where we require a given expected mean-payoff together with zero variance. Here we show that the problems can be all solved in polynomial time.

eess.SY↗
arXiv2012

Determinacy in Stochastic Games with Unbounded Payoff Functions

We consider infinite-state turn-based stochastic games of two players, Box and Diamond, who aim at maximizing and minimizing the expected total reward accumulated along a run, respectively. Since the total accumulated reward is unbounded, the determinacy of such games cannot be deduced directly from Martin's determinacy result for Blackwell games. Nevertheless, we show that these games are determined both for unrestricted (i.e., history-dependent and randomized) strategies and deterministic strategies, and the equilibrium value is the same. Further, we show that these games are generally not determined for memoryless strategies. Then, we consider a subclass of Diamond-finitely-branching games and show that they are determined for all of the considered strategy types, where the equilibrium value is always the same. We also examine the existence and type of (epsilon-)optimal strategies for both players.

cs.GT↗
arXiv2012

Efficient Controller Synthesis for Consumption Games with Multiple Resource Types

We introduce consumption games, a model for discrete interactive system with multiple resources that are consumed or reloaded independently. More precisely, a consumption game is a finite-state graph where each transition is labeled by a vector of resource updates, where every update is a non-positive number or omega. The omega updates model the reloading of a given resource. Each vertex belongs either to player \Box or player \Diamond, where the aim of player \Box is to play so that the resources are never exhausted. We consider several natural algorithmic problems about consumption games, and show that although these problems are computationally hard in general, they are solvable in polynomial time for every fixed number of resource types (i.e., the dimension of the update vectors).

cs.GT↗
arXiv2012

Minimizing Expected Termination Time in One-Counter Markov Decision Processes

We consider the problem of computing the value and an optimal strategy for minimizing the expected termination time in one-counter Markov decision processes. Since the value may be irrational and an optimal strategy may be rather complicated, we concentrate on the problems of approximating the value up to a given error epsilon > 0 and computing a finite representation of an epsilon-optimal strategy. We show that these problems are solvable in exponential time for a given configuration, and we also show that they are computationally hard in the sense that a polynomial-time approximation algorithm cannot exist unless P=NP.

cs.FL↗