About: Distributed Qualitative LTL Model Checking of Markov Decision Processes

Facets (new session)
Description
Metadata
Settings
- owl:sameAs
- Inference Rule:

About: Distributed Qualitative LTL Model Checking of Markov Decision Processes Goto Sponge NotDistinct Permalink

An Entity of Type : http://linked.opendata.cz/ontology/domain/vavai/Vysledek, within Data Space : linked.opendata.cz associated with source document(s)

Attributes	Values
rdf:type	skos:Concept http://linked.opendata.cz/ontology/domain/vavai/Vysledek
Description	Markov decision processes are used to model concurrent programs that exhibit uncertainty. The state explosion problem for probabilistic systems is more critical than in the non-probabilistic case. In the paper we propose a cluster-based algorithm for qualitative LTL model checking of finite state Markov decision processes. We use the automata approach which reduces the model checking problem to the question of existence of an accepting end component. The algorithm uses repeated reachability which systematically eliminates states that cannot belong to any accepting end component. A distinguished feature of the distributed algorithm is that its complexity meets the complexity of the best known sequential algorithm. Markov decision processes are used to model concurrent programs that exhibit uncertainty. The state explosion problem for probabilistic systems is more critical than in the non-probabilistic case. In the paper we propose a cluster-based algorithm for qualitative LTL model checking of finite state Markov decision processes. We use the automata approach which reduces the model checking problem to the question of existence of an accepting end component. The algorithm uses repeated reachability which systematically eliminates states that cannot belong to any accepting end component. A distinguished feature of the distributed algorithm is that its complexity meets the complexity of the best known sequential algorithm. (en)
Title	Distributed Qualitative LTL Model Checking of Markov Decision Processes Distributed Qualitative LTL Model Checking of Markov Decision Processes (en)
skos:prefLabel	Distributed Qualitative LTL Model Checking of Markov Decision Processes Distributed Qualitative LTL Model Checking of Markov Decision Processes (en)
skos:notation	RIV/00216224:14330/06:00015450!RIV10-GA0-14330___
http://linked.open...avai/riv/aktivita	P Z
http://linked.open...avai/riv/aktivity	P(1ET408050503), P(1M0545), P(GA201/06/1338), Z(MSM0021622419)
http://linked.open...vai/riv/dodaniDat	2010
http://linked.open...aciTvurceVysledku	Češka, Milan Černá, Ivana Barnat, Jiří Brim, Luboš Tůmová, Jana
http://linked.open.../riv/druhVysledku	D - Článek ve sborníku
http://linked.open...iv/duvernostUdaju	S - Úplné a pravdivé údaje nepodléhající ochraně podle zvláštních právních předpisů
http://linked.open...titaPredkladatele	Masarykova univerzita / Fakulta informatiky
http://linked.open...dnocenehoVysledku	471989
http://linked.open...ai/riv/idVysledku	RIV/00216224:14330/06:00015450
http://linked.open...riv/jazykVysledku	eng - angličtina
http://linked.open.../riv/klicovaSlova	distributed; parallel; LTL model checking; probabilistic systems; MDP (en)
http://linked.open.../riv/klicoveSlovo	LTL model checking MDP distributed parallel probabilistic systems
http://linked.open...ontrolniKodProRIV	[8C689997D5BA]
http://linked.open...v/mistoKonaniAkce	Bonn
http://linked.open...i/riv/mistoVydani	Bonn, Germany
http://linked.open...i/riv/nazevZdroje	Proceedings of 5th International Workshop on Parallel and Distributed Methods in verifiCation
http://linked.open...in/vavai/riv/obor	IN
http://linked.open...ichTvurcuVysledku	5 (xsd:int)
http://linked.open...cetTvurcuVysledku	5 (xsd:int)
http://linked.open...vavai/riv/projekt	Automated software verification Institute for Theoretical Computer Science Techniques for automatic verification and validation of software and hardware systems
http://linked.open...UplatneniVysledku	2006
http://linked.open...iv/tvurceVysledku	Barnat, Jiří Brim, Luboš Černá, Ivana Češka, Milan Tůmová, Jana
http://linked.open...vavai/riv/typAkce	WRD - Světová
http://linked.open.../riv/zahajeniAkce	2006-01-01 (xsd:date)
http://linked.open...n/vavai/riv/zamer	Highly Parallel and Distributed Computing Systems
issn	1571-0661
number of pages	15 (xsd:int)
http://purl.org/ne...btex#hasPublisher	University of Bonn
http://localhost/t...ganizacniJednotka	14330
is http://linked.open...avai/riv/vysledek of	Distributed Qualitative LTL Model Checking of Markov Decision Processes Distributed Qualitative LTL Model Checking of Markov Decision Processes

Faceted Search & Find service v1.16.118 as of Jun 21 2024

Alternative Linked Data Documents: ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 07.20.3240 as of Jun 21 2024, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (126 GB total memory, 58 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software