tr-announce

Download

tr-announce@lists.rwth-aachen.de

December 2007

1 participants
2 discussions

2007-22: Uncoordinated Two-Sided Markets
by Peter Schneider-Kamp 18 Dec '07

18 Dec '07

The following technical report is available from http://aib.informatik.rwth-aachen.de: Uncoordinated Two-Sided Markets Heiner Ackermann, Paul W. Goldberg, Vahab S. Mirrokni, Heiko Röglin, and Berthold Vöcking AIB 2007-22 Various economic interactions can be modeled as two-sided markets. A central solution concept to these markets are stable matchings, introduced by Gale and Shapley. It is well known that stable matchings can be computed in polynomial time, but many real-life markets lack a central authority to match agents. In those markets, matchings are formed by actions of self-interested agents. Knuth introduced uncoordinated two-sided markets and showed that the uncoordinated better response dynamics may cycle. However, Roth and Vande Vate showed that the random better response dynamics converges to a stable matching with probability one, but did not address the question of convergence time. In this paper, we give an exponential lower bound for the convergence time of the random better response dynamics in two-sided markets. We also extend these results to the best response dynamics, i.e., we present a cycle of best responses, and prove that the random best response dynamics converges to a stable matching with probability one, but its convergence time is exponential. Additionally, we identify the special class of correlated two-sided markets with real-life applications for which we prove that the random best response dynamics converges in expected polynomial time.

1 0

2007-20: Three-Valued Abstraction for Probabilistic Systems
by Peter Schneider-Kamp 04 Dec '07

04 Dec '07

The following technical report is available from http://aib.informatik.rwth-aachen.de: Three-Valued Abstraction for Probabilistic Systems Joost-Pieter Katoen, Daniel Klink, Martin Leucker, and Verena Wolf AIB 2007-20 This paper proposes a novel abstraction technique for fully probabilistic systems. The models of our study are classical discrete-time and continuous time Markov chains (DTMCs and CTMCs, for short). A DTMC is a Kripke structure in which each transition is equipped with a discrete probability; in a CTMC, in addition, state residence times are governed by negative exponential distributions. Our abstraction technique fits within the realm of three-valued abstraction methods that have been used successfully for traditional model checking. The key ingredients of our technique are a partitioning of the state space combined with an abstraction of transition probabilities by intervals. The uncertainty of intervals is resolved by history-dependent schedulers that may choose extreme values only. It is shown that this provides a conservative abstraction for both negative and affirmative verification results for a three-valued semantics of PCTL (Probabilistic Computation Tree Logic). In the continuous-time setting, the key idea is to apply abstraction on uniform CTMCs which are readily obtained from general CTMCs. In a similar way as for the discrete case, this is shown to yield a conservative abstraction for a three-valued semantics of CSL (Continuous Stochastic Logic). The verification of abstract DTMCs is inspired by the standard MDP (Markov Decision Process) model-checking problem. Abstract CTMCs can be verified by computing time-bounded reachability probabilities in continuous-time MDPs. Some experiments on an infinite-state stochastic Petri net indicate the feasibility of our abstraction technique.

1 0