#### Withdraw

Loading…

# Verification of linear-time properties for finite probabilistic systems

#### Kini, Dileep Raghunath

Loading…

## Permalink

https://hdl.handle.net/2142/99357

## Description

- Title
- Verification of linear-time properties for finite probabilistic systems
- Author(s)
- Kini, Dileep Raghunath
- Issue Date
- 2017-12-05
- Director of Research (if dissertation) or Advisor (if thesis)
- Viswanathan, Mahesh
- Doctoral Committee Chair(s)
- Viswanathan, Mahesh
- Committee Member(s)
- Agha, Gul
- Parthasarathy, Madhusudan
- Gulwani, Sumit

- Department of Study
- Computer Science
- Discipline
- Computer Science
- Degree Granting Institution
- University of Illinois at Urbana-Champaign
- Degree Name
- Ph.D.
- Degree Level
- Dissertation
- Keyword(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.
- Graduation Semester
- 2017-12
- Type of Resource
- text
- Permalink
- http://hdl.handle.net/2142/99357
- Copyright and License Information
- Copyright 2017 Dileep Kini

## Owning Collections

##### Graduate Dissertations and Theses at Illinois PRIMARY

Graduate Theses and Dissertations at Illinois##### Dissertations and Theses - Computer Science

Dissertations and Theses from the Dept. of Computer Science#### Manage Files

Loading…

#### Edit Collection Membership

Loading…

#### Edit Metadata

Loading…

#### Edit Properties

Loading…

#### Embargoes

Loading…