@inproceedings{1667, abstract = {We consider parametric version of fixed-delay continuoustime Markov chains (or equivalently deterministic and stochastic Petri nets, DSPN) where fixed-delay transitions are specified by parameters, rather than concrete values. Our goal is to synthesize values of these parameters that, for a given cost function, minimise expected total cost incurred before reaching a given set of target states. We show that under mild assumptions, optimal values of parameters can be effectively approximated using translation to a Markov decision process (MDP) whose actions correspond to discretized values of these parameters. To this end we identify and overcome several interesting phenomena arising in systems with fixed delays.}, author = {Brázdil, Tomáš and Korenčiak, L'Uboš and Krčál, Jan and Novotny, Petr and Řehák, Vojtěch}, location = {Madrid, Spain}, pages = {141 -- 159}, publisher = {Springer}, title = {{Optimizing performance of continuous-time stochastic systems using timeout synthesis}}, doi = {10.1007/978-3-319-22264-6_10}, volume = {9259}, year = {2015}, } @article{1673, abstract = {When a new mutant arises in a population, there is a probability it outcompetes the residents and fixes. The structure of the population can affect this fixation probability. Suppressing population structures reduce the difference between two competing variants, while amplifying population structures enhance the difference. Suppressors are ubiquitous and easy to construct, but amplifiers for the large population limit are more elusive and only a few examples have been discovered. Whether or not a population structure is an amplifier of selection depends on the probability distribution for the placement of the invading mutant. First, we prove that there exist only bounded amplifiers for adversarial placement-that is, for arbitrary initial conditions. Next, we show that the Star population structure, which is known to amplify for mutants placed uniformly at random, does not amplify for mutants that arise through reproduction and are therefore placed proportional to the temperatures of the vertices. Finally, we construct population structures that amplify for all mutational events that arise through reproduction, uniformly at random, or through some combination of the two. }, author = {Adlam, Ben and Chatterjee, Krishnendu and Nowak, Martin}, journal = {Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences}, number = {2181}, publisher = {Royal Society of London}, title = {{Amplifiers of selection}}, doi = {10.1098/rspa.2015.0114}, volume = {471}, year = {2015}, } @article{1681, abstract = {In many social situations, individuals endeavor to find the single best possible partner, but are constrained to evaluate the candidates in sequence. Examples include the search for mates, economic partnerships, or any other long-term ties where the choice to interact involves two parties. Surprisingly, however, previous theoretical work on mutual choice problems focuses on finding equilibrium solutions, while ignoring the evolutionary dynamics of decisions. Empirically, this may be of high importance, as some equilibrium solutions can never be reached unless the population undergoes radical changes and a sufficient number of individuals change their decisions simultaneously. To address this question, we apply a mutual choice sequential search problem in an evolutionary game-theoretical model that allows one to find solutions that are favored by evolution. As an example, we study the influence of sequential search on the evolutionary dynamics of cooperation. For this, we focus on the classic snowdrift game and the prisoner’s dilemma game.}, author = {Priklopil, Tadeas and Chatterjee, Krishnendu}, issn = {2073-4336}, journal = {Games}, number = {4}, pages = {413 -- 437}, publisher = {MDPI}, title = {{Evolution of decisions in population games with sequentially searching individuals}}, doi = {10.3390/g6040413}, volume = {6}, year = {2015}, } @inproceedings{1689, abstract = {We consider the problem of computing the set of initial states of a dynamical system such that there exists a control strategy to ensure that the trajectories satisfy a temporal logic specification with probability 1 (almost-surely). We focus on discrete-time, stochastic linear dynamics and specifications given as formulas of the Generalized Reactivity(1) fragment of Linear Temporal Logic over linear predicates in the states of the system. We propose a solution based on iterative abstraction-refinement, and turn-based 2-player probabilistic games. While the theoretical guarantee of our algorithm after any finite number of iterations is only a partial solution, we show that if our algorithm terminates, then the result is the set of satisfying initial states. Moreover, for any (partial) solution our algorithm synthesizes witness control strategies to ensure almost-sure satisfaction of the temporal logic specification. We demonstrate our approach on an illustrative case study.}, author = {Svoreňová, Mária and Kretinsky, Jan and Chmelik, Martin and Chatterjee, Krishnendu and Cěrná, Ivana and Belta, Cǎlin}, booktitle = {Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control}, location = {Seattle, WA, United States}, pages = {259 -- 268}, publisher = {ACM}, title = {{Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games}}, doi = {10.1145/2728606.2728608}, year = {2015}, } @inproceedings{1691, abstract = {We consider a case study of the problem of deploying an autonomous air vehicle in a partially observable, dynamic, indoor environment from a specification given as a linear temporal logic (LTL) formula over regions of interest. We model the motion and sensing capabilities of the vehicle as a partially observable Markov decision process (POMDP). We adapt recent results for solving POMDPs with parity objectives to generate a control policy. We also extend the existing framework with a policy minimization technique to obtain a better implementable policy, while preserving its correctness. The proposed techniques are illustrated in an experimental setup involving an autonomous quadrotor performing surveillance in a dynamic environment.}, author = {Svoreňová, Mária and Chmelik, Martin and Leahy, Kevin and Eniser, Hasan and Chatterjee, Krishnendu and Cěrná, Ivana and Belta, Cǎlin}, booktitle = {Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control}, location = {Seattle, WA, United States}, pages = {233 -- 238}, publisher = {ACM}, title = {{Temporal logic motion planning using POMDPs with parity objectives: Case study paper}}, doi = {10.1145/2728606.2728617}, year = {2015}, } @article{1694, abstract = { We introduce quantitative timed refinement and timed simulation (directed) metrics, incorporating zenoness checks, for timed systems. These metrics assign positive real numbers which quantify the timing mismatches between two timed systems, amongst non-zeno runs. We quantify timing mismatches in three ways: (1) the maximal timing mismatch that can arise, (2) the “steady-state” maximal timing mismatches, where initial transient timing mismatches are ignored; and (3) the (long-run) average timing mismatches amongst two systems. These three kinds of mismatches constitute three important types of timing differences. Our event times are the global times, measured from the start of the system execution, not just the time durations of individual steps. We present algorithms over timed automata for computing the three quantitative simulation distances to within any desired degree of accuracy. In order to compute the values of the quantitative simulation distances, we use a game theoretic formulation. We introduce two new kinds of objectives for two player games on finite-state game graphs: (1) eventual debit-sum level objectives, and (2) average debit-sum level objectives. We present algorithms for computing the optimal values for these objectives in graph games, and then use these algorithms to compute the values of the timed simulation distances over timed automata. }, author = {Chatterjee, Krishnendu and Prabhu, Vinayak}, journal = {IEEE Transactions on Automatic Control}, number = {9}, pages = {2291 -- 2306}, publisher = {IEEE}, title = {{Quantitative temporal simulation and refinement distances for timed systems}}, doi = {10.1109/TAC.2015.2404612}, volume = {60}, year = {2015}, } @article{1698, abstract = {In mean-payoff games, the objective of the protagonist is to ensure that the limit average of an infinite sequence of numeric weights is nonnegative. In energy games, the objective is to ensure that the running sum of weights is always nonnegative. Multi-mean-payoff and multi-energy games replace individual weights by tuples, and the limit average (resp., running sum) of each coordinate must be (resp., remain) nonnegative. We prove finite-memory determinacy of multi-energy games and show inter-reducibility of multi-mean-payoff and multi-energy games for finite-memory strategies. We improve the computational complexity for solving both classes with finite-memory strategies: we prove coNP-completeness improving the previous known EXPSPACE bound. For memoryless strategies, we show that deciding the existence of a winning strategy for the protagonist is NP-complete. We present the first solution of multi-mean-payoff games with infinite-memory strategies: we show that mean-payoff-sup objectives can be decided in NP∩coNP, whereas mean-payoff-inf objectives are coNP-complete.}, author = {Velner, Yaron and Chatterjee, Krishnendu and Doyen, Laurent and Henzinger, Thomas A and Rabinovich, Alexander and Raskin, Jean}, journal = {Information and Computation}, number = {4}, pages = {177 -- 196}, publisher = {Elsevier}, title = {{The complexity of multi-mean-payoff and multi-energy games}}, doi = {10.1016/j.ic.2015.03.001}, volume = {241}, year = {2015}, } @article{1709, abstract = {The competition for resources among cells, individuals or species is a fundamental characteristic of evolution. Biological all-pay auctions have been used to model situations where multiple individuals compete for a single resource. However, in many situations multiple resources with various values exist and single reward auctions are not applicable. We generalize the model to multiple rewards and study the evolution of strategies. In biological all-pay auctions the bid of an individual corresponds to its strategy and is equivalent to its payment in the auction. The decreasingly ordered rewards are distributed according to the decreasingly ordered bids of the participating individuals. The reproductive success of an individual is proportional to its fitness given by the sum of the rewards won minus its payments. Hence, successful bidding strategies spread in the population. We find that the results for the multiple reward case are very different from the single reward case. While the mixed strategy equilibrium in the single reward case with more than two players consists of mostly low-bidding individuals, we show that the equilibrium can convert to many high-bidding individuals and a few low-bidding individuals in the multiple reward case. Some reward values lead to a specialization among the individuals where one subpopulation competes for the rewards and the other subpopulation largely avoids costly competitions. Whether the mixed strategy equilibrium is an evolutionarily stable strategy (ESS) depends on the specific values of the rewards.}, author = {Reiter, Johannes and Kanodia, Ayush and Gupta, Raghav and Nowak, Martin and Chatterjee, Krishnendu}, journal = {Proceedings of the Royal Society of London Series B Biological Sciences}, number = {1812}, publisher = {Royal Society}, title = {{Biological auctions with multiple rewards}}, doi = {10.1098/rspb.2015.1041}, volume = {282}, year = {2015}, } @inproceedings{1714, abstract = {We present a flexible framework for the automated competitive analysis of on-line scheduling algorithms for firm-deadline real-time tasks based on multi-objective graphs: Given a task set and an on-line scheduling algorithm specified as a labeled transition system, along with some optional safety, liveness, and/or limit-average constraints for the adversary, we automatically compute the competitive ratio of the algorithm w.r.t. A clairvoyant scheduler. We demonstrate the flexibility and power of our approach by comparing the competitive ratio of several on-line algorithms, including Dover, that have been proposed in the past, for various task sets. Our experimental results reveal that none of these algorithms is universally optimal, in the sense that there are task sets where other schedulers provide better performance. Our framework is hence a very useful design tool for selecting optimal algorithms for a given application.}, author = {Chatterjee, Krishnendu and Pavlogiannis, Andreas and Kößler, Alexander and Schmid, Ulrich}, booktitle = {Real-Time Systems Symposium}, location = {Rome, Italy}, number = {January}, pages = {118 -- 127}, publisher = {IEEE}, title = {{A framework for automated competitive analysis of on-line scheduling of firm-deadline tasks}}, doi = {10.1109/RTSS.2014.9}, volume = {2015}, year = {2015}, } @article{1731, abstract = {We consider two-player zero-sum games on graphs. These games can be classified on the basis of the information of the players and on the mode of interaction between them. On the basis of information the classification is as follows: (a) partial-observation (both players have partial view of the game); (b) one-sided complete-observation (one player has complete observation); and (c) complete-observation (both players have complete view of the game). On the basis of mode of interaction we have the following classification: (a) concurrent (both players interact simultaneously); and (b) turn-based (both players interact in turn). The two sources of randomness in these games are randomness in transition function and randomness in strategies. In general, randomized strategies are more powerful than deterministic strategies, and randomness in transitions gives more general classes of games. In this work we present a complete characterization for the classes of games where randomness is not helpful in: (a) the transition function probabilistic transition can be simulated by deterministic transition); and (b) strategies (pure strategies are as powerful as randomized strategies). As consequence of our characterization we obtain new undecidability results for these games. }, author = {Chatterjee, Krishnendu and Doyen, Laurent and Gimbert, Hugo and Henzinger, Thomas A}, journal = {Information and Computation}, number = {12}, pages = {3 -- 16}, publisher = {Elsevier}, title = {{Randomness for free}}, doi = {10.1016/j.ic.2015.06.003}, volume = {245}, year = {2015}, } @inproceedings{1732, abstract = {We consider partially observable Markov decision processes (POMDPs), that are a standard framework for robotics applications to model uncertainties present in the real world, with temporal logic specifications. All temporal logic specifications in linear-time temporal logic (LTL) can be expressed as parity objectives. We study the qualitative analysis problem for POMDPs with parity objectives that asks whether there is a controller (policy) to ensure that the objective holds with probability 1 (almost-surely). While the qualitative analysis of POMDPs with parity objectives is undecidable, recent results show that when restricted to finite-memory policies the problem is EXPTIME-complete. While the problem is intractable in theory, we present a practical approach to solve the qualitative analysis problem. We designed several heuristics to deal with the exponential complexity, and have used our implementation on a number of well-known POMDP examples for robotics applications. Our results provide the first practical approach to solve the qualitative analysis of robot motion planning with LTL properties in the presence of uncertainty.}, author = {Chatterjee, Krishnendu and Chmelik, Martin and Gupta, Raghav and Kanodia, Ayush}, location = {Seattle, WA, United States}, pages = {325 -- 330}, publisher = {IEEE}, title = {{Qualitative analysis of POMDPs with temporal logic specifications for robotics applications}}, doi = {10.1109/ICRA.2015.7139019}, year = {2015}, } @inproceedings{1820, abstract = {We consider partially observable Markov decision processes (POMDPs) with a set of target states and every transition is associated with an integer cost. The optimization objec- tive we study asks to minimize the expected total cost till the target set is reached, while ensuring that the target set is reached almost-surely (with probability 1). We show that for integer costs approximating the optimal cost is undecidable. For positive costs, our results are as follows: (i) we establish matching lower and upper bounds for the optimal cost and the bound is double exponential; (ii) we show that the problem of approximating the optimal cost is decidable and present ap- proximation algorithms developing on the existing algorithms for POMDPs with finite-horizon objectives. While the worst- case running time of our algorithm is double exponential, we present efficient stopping criteria for the algorithm and show experimentally that it performs well in many examples.}, author = {Chatterjee, Krishnendu and Chmelik, Martin and Gupta, Raghav and Kanodia, Ayush}, booktitle = {Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence }, location = {Austin, TX, USA}, pages = {3496--3502}, publisher = {AAAI Press}, title = {{Optimal cost almost-sure reachability in POMDPs}}, volume = {5}, year = {2015}, } @inproceedings{1838, abstract = {Synthesis of program parts is particularly useful for concurrent systems. However, most approaches do not support common design tasks, like modifying a single process without having to re-synthesize or verify the whole system. Assume-guarantee synthesis (AGS) provides robustness against modifications of system parts, but thus far has been limited to the perfect information setting. This means that local variables cannot be hidden from other processes, which renders synthesis results cumbersome or even impossible to realize.We resolve this shortcoming by defining AGS under partial information. We analyze the complexity and decidability in different settings, showing that the problem has a high worstcase complexity and is undecidable in many interesting cases. Based on these observations, we present a pragmatic algorithm based on bounded synthesis, and demonstrate its practical applicability on several examples.}, author = {Bloem, Roderick and Chatterjee, Krishnendu and Jacobs, Swen and Könighofer, Robert}, location = {London, United Kingdom}, pages = {517 -- 532}, publisher = {Springer}, title = {{Assume-guarantee synthesis for concurrent reactive programs with partial information}}, doi = {10.1007/978-3-662-46681-0_50}, volume = {9035}, year = {2015}, } @inproceedings{1839, abstract = {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.}, author = {Brázdil, Tomáš and Chatterjee, Krishnendu and Forejt, Vojtěch and Kučera, Antonín}, location = {London, United Kingdom}, pages = {181 -- 187}, publisher = {Springer}, title = {{Multigain: A controller synthesis tool for MDPs with multiple mean-payoff objectives}}, doi = {10.1007/978-3-662-46681-0_12}, volume = {9035}, year = {2015}, } @article{1846, abstract = {Modal transition systems (MTS) is a well-studied specification formalism of reactive systems supporting a step-wise refinement methodology. Despite its many advantages, the formalism as well as its currently known extensions are incapable of expressing some practically needed aspects in the refinement process like exclusive, conditional and persistent choices. We introduce a new model called parametric modal transition systems (PMTS) together with a general modal refinement notion that overcomes many of the limitations. We investigate the computational complexity of modal and thorough refinement checking on PMTS and its subclasses and provide a direct encoding of the modal refinement problem into quantified Boolean formulae, allowing us to employ state-of-the-art QBF solvers for modal refinement checking. The experiments we report on show that the feasibility of refinement checking is more influenced by the degree of nondeterminism rather than by the syntactic restrictions on the types of formulae allowed in the description of the PMTS.}, author = {Beneš, Nikola and Kretinsky, Jan and Larsen, Kim and Möller, Mikael and Sickert, Salomon and Srba, Jiří}, journal = {Acta Informatica}, number = {2-3}, pages = {269 -- 297}, publisher = {Springer}, title = {{Refinement checking on parametric modal transition systems}}, doi = {10.1007/s00236-015-0215-4}, volume = {52}, year = {2015}, } @article{1851, abstract = {We consider mating strategies for females who search for males sequentially during a season of limited length. We show that the best strategy rejects a given male type if encountered before a time-threshold but accepts him after. For frequency-independent benefits, we obtain the optimal time-thresholds explicitly for both discrete and continuous distributions of males, and allow for mistakes being made in assessing the correct male type. When the benefits are indirect (genes for the offspring) and the population is under frequency-dependent ecological selection, the benefits depend on the mating strategy of other females as well. This case is particularly relevant to speciation models that seek to explore the stability of reproductive isolation by assortative mating under frequency-dependent ecological selection. We show that the indirect benefits are to be quantified by the reproductive values of couples, and describe how the evolutionarily stable time-thresholds can be found. We conclude with an example based on the Levene model, in which we analyze the evolutionarily stable assortative mating strategies and the strength of reproductive isolation provided by them.}, author = {Priklopil, Tadeas and Kisdi, Eva and Gyllenberg, Mats}, issn = {1558-5646}, journal = {Evolution}, number = {4}, pages = {1015 -- 1026}, publisher = {Wiley}, title = {{Evolutionarily stable mating decisions for sequentially searching females and the stability of reproductive isolation by assortative mating}}, doi = {10.1111/evo.12618}, volume = {69}, year = {2015}, } @article{1856, abstract = {The traditional synthesis question given a specification asks for the automatic construction of a system that satisfies the specification, whereas often there exists a preference order among the different systems that satisfy the given specification. Under a probabilistic assumption about the possible inputs, such a preference order is naturally expressed by a weighted automaton, which assigns to each word a value, such that a system is preferred if it generates a higher expected value. We solve the following optimal synthesis problem: given an omega-regular specification, a Markov chain that describes the distribution of inputs, and a weighted automaton that measures how well a system satisfies the given specification under the input assumption, synthesize a system that optimizes the measured value. For safety specifications and quantitative measures that are defined by mean-payoff automata, the optimal synthesis problem reduces to finding a strategy in a Markov decision process (MDP) that is optimal for a long-run average reward objective, which can be achieved in polynomial time. For general omega-regular specifications along with mean-payoff automata, the solution rests on a new, polynomial-time algorithm for computing optimal strategies in MDPs with mean-payoff parity objectives. Our algorithm constructs optimal strategies that consist of two memoryless strategies and a counter. The counter is in general not bounded. To obtain a finite-state system, we show how to construct an ε-optimal strategy with a bounded counter, for all ε > 0. Furthermore, we show how to decide in polynomial time if it is possible to construct an optimal finite-state system (i.e., a system without a counter) for a given specification. We have implemented our approach and the underlying algorithms in a tool that takes qualitative and quantitative specifications and automatically constructs a system that satisfies the qualitative specification and optimizes the quantitative specification, if such a system exists. We present some experimental results showing optimal systems that were automatically generated in this way.}, author = {Chatterjee, Krishnendu and Henzinger, Thomas A and Jobstmann, Barbara and Singh, Rohit}, journal = {Journal of the ACM}, number = {1}, publisher = {ACM}, title = {{Measuring and synthesizing systems in probabilistic environments}}, doi = {10.1145/2699430}, volume = {62}, year = {2015}, } @article{1873, abstract = {We consider partially observable Markov decision processes (POMDPs) with limit-average payoff, where a reward value in the interval [0,1] is associated with every transition, and the payoff of an infinite path is the long-run average of the rewards. We consider two types of path constraints: (i) a quantitative constraint defines the set of paths where the payoff is at least a given threshold λ1ε(0,1]; and (ii) a qualitative constraint which is a special case of the quantitative constraint with λ1=1. We consider the computation of the almost-sure winning set, where the controller needs to ensure that the path constraint is satisfied with probability 1. Our main results for qualitative path constraints are as follows: (i) the problem of deciding the existence of a finite-memory controller is EXPTIME-complete; and (ii) the problem of deciding the existence of an infinite-memory controller is undecidable. For quantitative path constraints we show that the problem of deciding the existence of a finite-memory controller is undecidable. We also present a prototype implementation of our EXPTIME algorithm and experimental results on several examples.}, author = {Chatterjee, Krishnendu and Chmelik, Martin}, journal = {Artificial Intelligence}, pages = {46 -- 72}, publisher = {Elsevier}, title = {{POMDPs under probabilistic semantics}}, doi = {10.1016/j.artint.2014.12.009}, volume = {221}, year = {2015}, } @inproceedings{1882, abstract = {We provide a framework for compositional and iterative design and verification of systems with quantitative information, such as rewards, time or energy. It is based on disjunctive modal transition systems where we allow actions to bear various types of quantitative information. Throughout the design process the actions can be further refined and the information made more precise. We show how to compute the results of standard operations on the systems, including the quotient (residual), which has not been previously considered for quantitative non-deterministic systems. Our quantitative framework has close connections to the modal nu-calculus and is compositional with respect to general notions of distances between systems and the standard operations.}, author = {Fahrenberg, Uli and Kretinsky, Jan and Legay, Axel and Traonouez, Louis}, location = {Bertinoro, Italy}, pages = {306 -- 324}, publisher = {Springer}, title = {{Compositionality for quantitative specifications}}, doi = {10.1007/978-3-319-15317-9_19}, volume = {8997}, year = {2015}, } @article{2034, abstract = {Opacity is a generic security property, that has been defined on (non-probabilistic) transition systems and later on Markov chains with labels. For a secret predicate, given as a subset of runs, and a function describing the view of an external observer, the value of interest for opacity is a measure of the set of runs disclosing the secret. We extend this definition to the richer framework of Markov decision processes, where non-deterministicchoice is combined with probabilistic transitions, and we study related decidability problems with partial or complete observation hypotheses for the schedulers. We prove that all questions are decidable with complete observation and ω-regular secrets. With partial observation, we prove that all quantitative questions are undecidable but the question whether a system is almost surely non-opaquebecomes decidable for a restricted class of ω-regular secrets, as well as for all ω-regular secrets under finite-memory schedulers.}, author = {Bérard, Béatrice and Chatterjee, Krishnendu and Sznajder, Nathalie}, journal = { Information Processing Letters}, number = {1}, pages = {52 -- 59}, publisher = {Elsevier}, title = {{Probabilistic opacity for Markov decision processes}}, doi = {10.1016/j.ipl.2014.09.001}, volume = {115}, year = {2015}, }