1,721,336 research outputs found
Compositional Quantitative Reasoning * Krishnendu Chatterjee
No full textUC Los Angeles Mari"elle StoelingaUniversity of Twente Abstract. We present a compositional theory of system verifica-tion, where specifications assign real-numbered costs to systems. These costs can express a wide variety of quantitative system prop-erties, such as resource consumption, price, or a measure of how well a system satisfies its specification. The theory supports thecomposition of systems and specifications, and the hiding of variables. Boolean refinement relations are replaced by real-numbereddistances between descriptions of a system at different levels of detail. We show that the classical boolean rules for compositionalreasoning have quantitative counterparts in our setting
Faster Algorithms for Alternating Refinement Relations
Full text linkOne central issue in the formal design and analysis of reactive systems is the notion of refinement that asks whether all behaviors of the implementation is allowed by the specification. The local interpretation of behavior leads to the notion of simulation. Alternating transition systems (ATSs) provide a general model for composite reactive systems, and the simulation relation for ATSs is known as alternating simulation. The simulation relation for fair transition systems is called fair simulation. In this work our main contributions are as follows: (1) We present an improved algorithm for fair simulation with Büchi fairness constraints; our algorithm requires O(n^3 * m) time as compared to the previous known O(n^6)-time algorithm, where n is the number of states and m is the number of transitions. (2) We present a game based algorithm for alternating simulation that requires O(m^2)-time as compared to the previous known O((n*m)^2)-time algorithm, where n is the number of states and m is the size of transition relation. (3) We present an iterative algorithm for alternating simulation that matches the time complexity of the game based algorithm, but is more space efficient than the game based algorithm
What is Decidable about Partially Observable Markov Decision Processes with omega-Regular Objectives
Full text linkWe consider partially observable Markov decision processes (POMDPs) with omega-regular conditions specified as parity objectives. The qualitative analysis problem given a POMDP 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, we establish decidability (with optimal EXPTIME-complete complexity) of the qualitative analysis problems for POMDPs with all parity objectives under finite-memory strategies. We also establish optimal (exponential) memory bounds
Computer code for "Efficiency and resilience of cooperation in asymmetric social dilemmas"
No full textin the research article "Efficiency and resilience of cooperation in asymmetric social dilemmas" (by Valentin Hübner, Manuel Staab, Christian Hilbe, Krishnendu Chatterjee, and Maria Kleshnina).
We used different implementations for the case of two and three players, both described below
Algorithms for Game Metrics
Full text linkSimulation 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 -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 the one-step metric distance between states.
The algorithm improves on the
previously known exponential-time algorithm based on a reduction to the theory of
reals.
We then present PSPACE algorithms for both the decision problem and the
problem of approximating the metric distance between two states,
matching the best known bound for Markov chains.
For the bisimulation kernel of the metric, which corresponds to probabilistic
bisimulation, our algorithm works in time \calo(n^4) for both
turn-based games and MDPs; improving the previously best known
\calo(n^9\cdot\log(n)) time algorithm for MDPs.
For a concurrent game , we show that computing the exact distance
between states is at least as hard as computing the value of
concurrent reachability games and
the square-root-sum problem in computational geometry.
We show that checking whether the metric distance is bounded by a
rational , can be accomplished via a reduction to the theory of
real closed fields, involving a formula with three quantifier
alternations, yielding \calo(|G|^{\calo(|G|^5)}) time
complexity, improving the previously known reduction with
\calo(|G|^{\calo(|G|^7)}) time complexity.
These algorithms can be iterated to approximate the metrics using
binary search
Going Beyond Counting First Authors in Author Co-citation Analysis
Full text linkThe present study examines one of the fundamental aspects of author co-citation analysis (ACA) - the way co-citation
counts are defined. Co-citation counting provides the data on which all subsequent statistical analyses and mappings
are based, and we compare ACA results based on two different types of co-citation counting - the traditional type that
only counts the first one among a cited work's authors on the one hand and a non-traditional type that takes into
account the first 5 authors of a cited work on the other hand. Results indicate that the picture produced through this non-traditional author co-citation counting contains more coherent author groups and is therefore considerably clearer. However, this picture represents fewer specialties in the research field being studied than that produced through the traditional first-author co-citation counting when the same number of top-ranked authors is selected and analyzed. Reasons for these effects are discussed
Combinations of Qualitative Winning for Stochastic Parity Games
Full text linkWe study Markov decision processes and turn-based stochastic games with parity conditions. There are three qualitative winning criteria, namely, sure winning, which requires all paths to satisfy the condition, almost-sure winning, which requires the condition to be satisfied with probability 1, and limit-sure winning, which requires the condition to be satisfied with probability arbitrarily close to 1. We study the combination of two of these criteria for parity conditions, e.g., there are two parity conditions one of which must be won surely, and the other almost-surely. The problem has been studied recently by Berthon et al. for MDPs with combination of sure and almost-sure winning, under infinite-memory strategies, and the problem has been established to be in NP cap co-NP. Even in MDPs there is a difference between finite-memory and infinite-memory strategies. Our main results for combination of sure and almost-sure winning are as follows: (a) we show that for MDPs with finite-memory strategies the problem is in NP cap co-NP; (b) we show that for turn-based stochastic games the problem is co-NP-complete, both for finite-memory and infinite-memory strategies; and (c) we present algorithmic results for the finite-memory case, both for MDPs and turn-based stochastic games, by reduction to non-stochastic parity games. In addition we show that all the above complexity results also carry over to combination of sure and limit-sure winning, and results for all other combinations can be derived from existing results in the literature. Thus we present a complete picture for the study of combinations of two qualitative winning criteria for parity conditions in MDPs and turn-based stochastic games
Computation Tree Logic for Synchronization Properties
Full text linkWe 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 hard for the class of problems solvable in polynomial time using a parallel access to an NP oracle. 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
- …
