About: Local Quantitative LTL Model Checking

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

About: Local Quantitative LTL Model Checking 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	Quantitative analysis of probabilistic systems has been studied mainly from the global model checking point, of view. In the global model-checking, the goal of verification is to decide the probability of satisfaction of a given property for all reachable states in the state space of the system under investigation. On the other hand, in local model checking approach the probability of satisfaction is computed only for the set of initial states. In theory, it is possible to solve the local model checking problem using the global model checking approach. However, the global model checking procedure call be significantly outperformed by a dedicated local model checking one. In this paper we present several particular local model checking techniques that, if applied to global model checking procedure reduce the runtime needed from days to minutes. Quantitative analysis of probabilistic systems has been studied mainly from the global model checking point, of view. In the global model-checking, the goal of verification is to decide the probability of satisfaction of a given property for all reachable states in the state space of the system under investigation. On the other hand, in local model checking approach the probability of satisfaction is computed only for the set of initial states. In theory, it is possible to solve the local model checking problem using the global model checking approach. However, the global model checking procedure call be significantly outperformed by a dedicated local model checking one. In this paper we present several particular local model checking techniques that, if applied to global model checking procedure reduce the runtime needed from days to minutes. (en)
Title	Local Quantitative LTL Model Checking Local Quantitative LTL Model Checking (en)
skos:prefLabel	Local Quantitative LTL Model Checking Local Quantitative LTL Model Checking (en)
skos:notation	RIV/00216224:14330/09:00065775!RIV14-GA0-14330___
http://linked.open...avai/riv/aktivita	P
http://linked.open...avai/riv/aktivity	P(1ET408050503), P(1M0545), P(GA201/06/1338)
http://linked.open...vai/riv/dodaniDat	2014
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	323987
http://linked.open...ai/riv/idVysledku	RIV/00216224:14330/09:00065775
http://linked.open...riv/jazykVysledku	eng - angličtina
http://linked.open.../riv/klicovaSlova	Quantitative Model Checking; Linear Temporal Logic; Probabilistic systems (en)
http://linked.open.../riv/klicoveSlovo	Probabilistic systems Linear Temporal Logic Quantitative Model Checking
http://linked.open...ontrolniKodProRIV	[7A9B1798F7DD]
http://linked.open...v/mistoKonaniAkce	L'Aquila, Italy
http://linked.open...i/riv/mistoVydani	Neuveden
http://linked.open...i/riv/nazevZdroje	Formal Methods for Industrial Critical Systems
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	2009
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...ain/vavai/riv/wos	000270704100004
http://linked.open.../riv/zahajeniAkce	2008-01-01 (xsd:date)
issn	0302-9743
number of pages	16 (xsd:int)
http://bibframe.org/vocab/doi	10.1007/978-3-642-03240-0_8
http://purl.org/ne...btex#hasPublisher	Springer-Verlag. (Berlin; Heidelberg)
https://schema.org/isbn	9783642032394
http://localhost/t...ganizacniJednotka	14330

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