Abstract
Fundamental algorithmic problems that lie in the core of many application in formal verification and analysis of systems can be described as graphrelated algorithmic problems. Nodes in these problems are of one of two (or three) types, giving rise to a gametheoretic viewpoint: Player one nodes are under the control of the algorithm that wants to accomplish a goal, player two nodes are under the control of a worstcase adversary that tries to keep player one to achieve her goal, and random nodes are under the control of a random process that is oblivious to the goal of player one. A graph containing only player one and random nodes is called a Markov Decision Process, a graph containing only player one and player two nodes is called a game graph. A variety of goals on these graphs are of interest, the simplest being whether a fixed set of nodes can be reached. The algorithmic question is then whether there is a strategy for player one to achieve her goal from a given starting node. In this talk we give an overview of a variety of goals that are interesting in computeraided verification and present upper and (conditional) lower bounds on the time complexity for deciding whether a winning strategy for player one exists.
BibTeX  Entry
@InProceedings{henzinger:LIPIcs:2017:7505,
author = {Monika Henzinger},
title = {{Efficient Algorithms for GraphRelated Problems in ComputerAided Verification (Invited Talk)}},
booktitle = {44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)},
pages = {2:12:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959770415},
ISSN = {18688969},
year = {2017},
volume = {80},
editor = {Ioannis Chatzigiannakis and Piotr Indyk and Fabian Kuhn and Anca Muscholl},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2017/7505},
URN = {urn:nbn:de:0030drops75054},
doi = {10.4230/LIPIcs.ICALP.2017.2},
annote = {Keywords: Computeraided Verification, Game Theory, Markov Decision Process}
}
Keywords: 

Computeraided Verification, Game Theory, Markov Decision Process 
Collection: 

44th International Colloquium on Automata, Languages, and Programming (ICALP 2017) 
Issue Date: 

2017 
Date of publication: 

07.07.2017 