tr-announce December 2007

tr-announce@lists.rwth-aachen.de

1 participants
2 discussions

2007-22: Uncoordinated Two-Sided Markets

by Peter Schneider-Kamp

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.

16 years, 9 months

2007-20: Three-Valued Abstraction for Probabilistic Systems

by Peter Schneider-Kamp

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.

16 years, 9 months

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

2003

2002

2001

tr-announce December 2007