About: Randomization Helps in 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)

AttributesValues
rdf:type
Description
  • We present and analyze a new probabilistic method for automata based LTL model checking of non-proba\-bi\-listic systems with intention to reduce memory requirements. The main idea of our approach is to use randomness to decide which of the needed information (visited states) should be stored during a computation and which could be omitted. We propose two strategies of probabilistic storing of states. The algorithm never errs, i.e. it always delivers correct results. On the other hand the computation time can increase. The method has been embedded into the SPIN model checker and a series of experiments has been performed. The results confirm that randomization can help to increase the applicability of model checkers in practice.
  • We present and analyze a new probabilistic method for automata based LTL model checking of non-proba\-bi\-listic systems with intention to reduce memory requirements. The main idea of our approach is to use randomness to decide which of the needed information (visited states) should be stored during a computation and which could be omitted. We propose two strategies of probabilistic storing of states. The algorithm never errs, i.e. it always delivers correct results. On the other hand the computation time can increase. The method has been embedded into the SPIN model checker and a series of experiments has been performed. The results confirm that randomization can help to increase the applicability of model checkers in practice. (en)
Title
  • Randomization Helps in LTL Model Checking
  • Randomization Helps in LTL Model Checking (en)
skos:prefLabel
  • Randomization Helps in LTL Model Checking
  • Randomization Helps in LTL Model Checking (en)
skos:notation
  • RIV/00216224:14330/01:00004526!RIV/2002/GA0/143302/N
http://linked.open.../vavai/riv/strany
  • 105
http://linked.open...avai/riv/aktivita
http://linked.open...avai/riv/aktivity
  • P(GA201/00/0400), P(GA201/00/1023), Z(MSM 143300001)
http://linked.open...vai/riv/dodaniDat
http://linked.open...aciTvurceVysledku
http://linked.open.../riv/druhVysledku
http://linked.open...iv/duvernostUdaju
http://linked.open...titaPredkladatele
http://linked.open...dnocenehoVysledku
  • 693931
http://linked.open...ai/riv/idVysledku
  • RIV/00216224:14330/01:00004526
http://linked.open...riv/jazykVysledku
http://linked.open.../riv/klicovaSlova
  • Model checking, randomized algorithm, depth-first search (en)
http://linked.open.../riv/klicoveSlovo
http://linked.open...ontrolniKodProRIV
  • [290AAF3664C6]
http://linked.open...v/mistoKonaniAkce
  • Berlin Heidelberg New York
http://linked.open...i/riv/mistoVydani
  • Berlin Heidelberg New York
http://linked.open...i/riv/nazevZdroje
  • Process Algebra and Probabilistic Methods. Proceedings of PAPM-PROBMIV 2001
http://linked.open...in/vavai/riv/obor
http://linked.open...ichTvurcuVysledku
http://linked.open...cetTvurcuVysledku
http://linked.open...ocetUcastnikuAkce
http://linked.open...nichUcastnikuAkce
http://linked.open...vavai/riv/projekt
http://linked.open...UplatneniVysledku
http://linked.open...iv/tvurceVysledku
  • Brim, Luboš
  • Černá, Ivana
  • Nečesal, Martin
http://linked.open...vavai/riv/typAkce
http://linked.open.../riv/zahajeniAkce
http://linked.open...n/vavai/riv/zamer
number of pages
http://purl.org/ne...btex#hasPublisher
  • Springer-Verlag
https://schema.org/isbn
  • 3-540-42556-X
http://localhost/t...ganizacniJednotka
  • 14330
Faceted Search & Find service v1.16.118 as of Jun 21 2024


Alternative Linked Data Documents: ODE     Content Formats:   [cxml] [csv]     RDF   [text] [turtle] [ld+json] [rdf+json] [rdf+xml]     ODATA   [atom+xml] [odata+json]     Microdata   [microdata+json] [html]    About   
This material is Open Knowledge   W3C Semantic Web Technology [RDF Data] Valid XHTML + RDFa
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