Files in this item

FilesDescriptionFormat

application/pdf

application/pdfKINI-DISSERTATION-2017.pdf (2MB)
(no description provided)PDF

Description

Title:Verification of linear-time properties for finite probabilistic systems
Author(s):Kini, Dileep Raghunath
Director of Research:Viswanathan, Mahesh
Doctoral Committee Chair(s):Viswanathan, Mahesh
Doctoral Committee Member(s):Agha, Gul; Parthasarathy, Madhusudan; Gulwani, Sumit
Department / Program:Computer Science
Discipline:Computer Science
Degree Granting Institution:University of Illinois at Urbana-Champaign
Degree:Ph.D.
Genre:Dissertation
Subject(s):Probabilistic model checking
Markov decision processes
Linear temporal logic
Automata theory
Abstract:With computers becoming ubiquitous there is an ever growing necessity to ensure that they are programmed to behave correctly. Formal verification is a discipline within computer science that tackles issues related to design and analysis of programs with the aim of producing well behaved systems. One of the core problems in this domain is what is called the model checking problem: given a mathematical model of a computer and a correctness specification, does the model satisfy the specification? In this thesis we explore this question for Markov Decision Processes (MDPs), which are finite state models involving stochastic and non-deterministic behaviour over discrete time steps. The kind of specifications we focus on are those that describe the correctness of individual executions of the model, called linear time properties. We delve into two different semantics for assigning meaning to the model checking problem: execution based semantics and distribution based semantics. In the execution based semantics we look at specifications described using Linear Temporal Logic (LTL). The model checking problem under this semantics are of two kinds: qualitative and quantitative. In the qualitative version we are interested in finding out if the specification is satisfied with non-zero probability, and in the more general quantitative version we want to know whether the probability of satisfaction is greater than a given quantity. The standard way to do model checking for both cases involves translating the LTL formula into an automaton which is then used to analyze the given MDP. One of the contributions of this thesis is a new translation of LTL to automata that are provably smaller than previously known ones. This translation helps us in reducing the asymptotic complexity of qualitative model checking of MDPs against certain fragments of LTL. We implement this translation in a tool called Büchifier to show its benefits on real examples. Our second main contribution involves a new automata-based algorithm for quantitative model checking that along with known translations of LTL to automata, which gives us new complexity results for the problem for different fragments of LTL. In the distribution based semantics we view MDPs as producing a sequence of probability distributions over its state space. At each point of time we are interested in the truth of atomic propositions, each of which tells us whether the probability of being in a certain states is above or below a given threshold. Linear time properties over these propositions are then used to describe correctness criteria. The model checking problem here happens to be undecidable in general, and therefore we consider restrictions on the problem. First we consider propositions which are robust: a proposition is said to be robust when the probability of being in its associated set of states is always well separated from its given threshold. For properties described over such propositions we observe that the model checking problem becomes decidable. But checking for robustness itself is an undecidable problem for MDPs. So we focus our attention on a subclass of MDPs called Markov Chains which exhibit stochastic behaviour without non-determinism. For Markov Chains we show that checking for robustness and model checking under robustness become tractable and we provide an analysis of the computational complexity of these problems.
Issue Date:2017-12-05
Type:Text
URI:http://hdl.handle.net/2142/99357
Rights Information:Copyright 2017 Dileep Kini
Date Available in IDEALS:2018-03-13
Date Deposited:2017-12


This item appears in the following Collection(s)

Item Statistics