h1

% IMPORTANT: The following is UTF-8 encoded.  This means that in the presence
% of non-ASCII characters, it will not work with BibTeX 0.99 or older.
% Instead, you should use an up-to-date BibTeX implementation like “bibtex8” or
% “biber”.

@PHDTHESIS{Chakraborty:761892,
      author       = {Chakraborty, Souymodip},
      othercontributors = {Katoen, Joost-Pieter and Zhang, Lijun},
      title        = {{N}ew results on probabilistic verification : automata,
                      logic and satisfiability},
      school       = {RWTH Aachen University},
      type         = {Dissertation},
      address      = {Aachen},
      reportid     = {RWTH-2019-05211},
      pages        = {1 Online-Ressource (172 Seiten) : Illustrationen},
      year         = {2019},
      note         = {Veröffentlicht auf dem Publikationsserver der RWTH Aachen
                      University; Dissertation, RWTH Aachen University, 2019},
      abstract     = {Probabilistic (or quantitative) verification is a branch of
                      formal methods dealing with stochastic models and logic.
                      Probabilistic models capture the behavior of randomized
                      algorithms and other physical systems with certain
                      uncertainty, whereas probabilistic logic expresses the
                      quantitative measure on the probabilistic space defined by
                      the models. Most often, the formal techniques used in
                      studying the behavior of these models and logic are not just
                      mundane extension of its non-probabilistic counterparts. The
                      complexity of these mathematical structures is surprisingly
                      different. The thesis is an effort at improving our
                      continued under- standing of these models and logic. We will
                      begin by looking at few interesting formal representations
                      of discrete stochastic models. Namely, we will address the
                      parameter synthesis problem for parametric linear time
                      temporal logic and model checking of convex Markov decision
                      processes with open intervals. The primary focus of the
                      thesis is however on the satisfiability (or validity)
                      problem of different probabilistic logics. This includes a
                      bounded fragment of probabilistic logic and a simple
                      quantitative (probabilistic) extension of mu-calculus.
                      Decision procedures for the satisfiability problems are
                      developed and a detailed complexity analysis of these
                      problems is provided. The study of automata has been very
                      effective in understanding logic. We will look at the newly
                      conceived notion of p-automata, which are a probabilistic
                      extension of alternating tree automata. As we will see,
                      probabilistic logic exhibits both non-deterministic and
                      stochastic behavior. The semantics of p-automata are
                      extended to capture non-determinism and hence model Markov
                      decision processes.},
      cin          = {121310 / 120000},
      ddc          = {004},
      cid          = {$I:(DE-82)121310_20140620$ / $I:(DE-82)120000_20140620$},
      typ          = {PUB:(DE-HGF)11},
      doi          = {10.18154/RWTH-2019-05211},
      url          = {https://publications.rwth-aachen.de/record/761892},
}