• Recursive markov decision proc...

Result: Recursive markov decision processes and recursive stochastic games

Title:
Recursive markov decision processes and recursive stochastic games
Authors:
ETESSAMI, Kousha, YANNAKAKIS, Mihalis
Source:
Automata, languages and programming (Lisbon, 11-15 July 2005)Lecture notes in computer science. :891-903
Publisher Information:
Berlin: Springer, 2005.
Publication Year:
2005
Physical Description:
print, 1 p.1/4
Original Material:
INIST-CNRS
Subject Terms:
Computer science, Informatique, Sciences exactes et technologie, Exact sciences and technology, Sciences appliquees, Applied sciences, Informatique; automatique theorique; systemes, Computer science; control theory; systems, Informatique théorique, Theoretical computing, Automates. Machines abstraites. Machines de turing, Automata. Abstract machines. Turing machines, Approche probabiliste, Probabilistic approach, Enfoque probabilista, Automate à pile, Push down automaton, Autómata a pila, Borne inférieure, Lower bound, Cota inferior, Borne supérieure, Upper bound, Cota superior, Chaîne Markov, Markov chain, Cadena Markov, Complexité algorithme, Algorithm complexity, Complejidad algoritmo, Décidabilité, Decidability, Decidibilidad, Décision Markov, Markov decision, Decisión Markov, Grammaire CF, Context free grammar, Gramática independiente, Jeu stochastique, Stochastic game, Juego estocástico, Modèle Markov, Markov model, Modelo Markov, Modélisation, Modeling, Modelización, Non déterminisme, Non determinism, No determinismo, Problème terminaison, Termination problem, Problema terminación, Processus Markov, Markov process, Proceso Markov, Processus branchement, Branching process, Proceso ramificación, Processus stochastique, Stochastic process, Proceso estocástico, Stratégie joueur, Player strategy, Estrategia jugador, Système interaction, Interaction system, Sistema interacción, Vérification modèle, Model checking, Verificación modelo, Vérification programme, Program verification, Verificación programa
Document Type:
Conference Conference Paper
File Description:
text
Language:
English
Author Affiliations:
LFCS, School of Informatics, University of Edinburgh, United Kingdom
Department of Computer Science, Columbia University, United States
ISSN:
0302-9743
Access URL:
http://pascal-francis.inist.fr/vibad/index.php?action=search&terms=16991856
Rights:
Copyright 2005 INIST-CNRS
CC BY 4.0
Sauf mention contraire ci-dessus, le contenu de cette notice bibliographique peut être utilisé dans le cadre d’une licence CC BY 4.0 Inist-CNRS / Unless otherwise stated above, the content of this bibliographic record may be used under a CC BY 4.0 licence by Inist-CNRS / A menos que se haya señalado antes, el contenido de este registro bibliográfico puede ser utilizado al amparo de una licencia CC BY 4.0 Inist-CNRS
Notes:
Computer science; theoretical automation; systems
Accession Number:
edscal.16991856
Database:
PASCAL Archive

Further Information

We introduce Recursive Markov Decision Processes (RMDPs) and Recursive Simple Stochastic Games (RSSGs), and study the decidability and complexity of algorithms for their analysis and verification. These models extend Recursive Markov Chains (RMCs), introduced in [EY05a, EY05b] as a natural model for verification of probabilistic procedural programs and related systems involving both recursion and probabilistic behavior. RMCs define a class of denumerable Markov chains with a rich theory generalizing that of stochastic context-free grammars and multi-type branching processes, and they are also intimately related to probabilistic pushdown systems. RMDPs & RSSGs extend RMCs with one controller or two adversarial players, respectively. Such extensions are useful for modeling nondeterministic and concurrent behavior, as well as modeling a system's interactions with an environment. We provide upper and lower bounds for deciding, given an RMDP (or RSSG) A and probability p, whether player 1 has a strategy to force termination at a desired exit with probability at least p. We also address qualitative termination, where p = 1, and model checking questions.