Informatik-Logo Technischen Berichte der
Fakultät für Informatik
der
Technischen Universität München
TUM-Logo

[Übersicht]    [Suchen]    [Ausgewählte Publikationen Ausgewählte Publikationen]
Suche: Citkey="TUM-I0519"
Als [bib] [pdf] [ps] [dvi] [xml]  herunterladen.

Don't know in Probabilistic Systems Publikation auswählen
Martin Leucker, Verena Wolf Harald Fecher
Technical Report, 2005

 
Revision-Date:  2005-10-01
Category:  Technical Report, TUM-I0519
Format:   Postscript, gzipped
PDF, gzipped
 
Abstract:  This work extends the abstraction-refinement paradigm based on 3-valued logics to the setting of probabilistic systems. Firstly, We define a notion of abstraction for Markov chains. To be able to relate the behavior of abstract and concrete systems, we equip the notion of abstraction with the concept of simulation.
Furthermore, we present model checking for abstract probabilistic systems (abstract Markov chains) with respect to specifications in probabilistic temporal logics, interpreted over a 3-valued domain. More specifically, we introduce a 3-valued version of probabilistic computation-tree logic (PCTL) and give a model checking algorithm w.r.t. abstract Markov chains.
 
 
Classification:  F.3,G.3
 
Keywords:   Abstraction, Model Checking, 3-valued logic
 
Version:  1.0
Length:  16 Pages
URL:   http://drehscheibe.in.tum.de/forschung/pub/reports/2005/TUM-I0519.ps.gz
http://drehscheibe.in.tum.de/forschung/pub/reports/2005/TUM-I0519.pdf.gz