About: Is there a best Büchi automaton for explicit 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
  • LTL to Büchi automata (BA) translators are traditionally optimized to produce automata with a small number of states or a small number of non-deterministic states. In this paper, we search for properties of Büchi automata that really influence the performance of explicit model checkers. We do that by manual analysis of several automata and by experiments with common LTL-to-BA translators and realistic verification tasks. As a result of these experiences, we gain a better insight into the characteristics of automata that work well with Spin.
  • LTL to Büchi automata (BA) translators are traditionally optimized to produce automata with a small number of states or a small number of non-deterministic states. In this paper, we search for properties of Büchi automata that really influence the performance of explicit model checkers. We do that by manual analysis of several automata and by experiments with common LTL-to-BA translators and realistic verification tasks. As a result of these experiences, we gain a better insight into the characteristics of automata that work well with Spin. (en)
Title
  • Is there a best Büchi automaton for explicit model checking?
  • Is there a best Büchi automaton for explicit model checking? (en)
skos:prefLabel
  • Is there a best Büchi automaton for explicit model checking?
  • Is there a best Büchi automaton for explicit model checking? (en)
skos:notation
  • RIV/00216224:14330/14:00073815!RIV15-MSM-14330___
http://linked.open...avai/riv/aktivita
http://linked.open...avai/riv/aktivity
  • I, P(GBP202/12/G061), S
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
  • 22920
http://linked.open...ai/riv/idVysledku
  • RIV/00216224:14330/14:00073815
http://linked.open...riv/jazykVysledku
http://linked.open.../riv/klicovaSlova
  • linear temporal logic; Büchi automata; explicit model checking (en)
http://linked.open.../riv/klicoveSlovo
http://linked.open...ontrolniKodProRIV
  • [5BA13207A905]
http://linked.open...v/mistoKonaniAkce
  • San Jose, CA, USA
http://linked.open...i/riv/mistoVydani
  • New York
http://linked.open...i/riv/nazevZdroje
  • 2014 International SPIN Symposium on Model Checking of Software
http://linked.open...in/vavai/riv/obor
http://linked.open...ichTvurcuVysledku
http://linked.open...cetTvurcuVysledku
http://linked.open...vavai/riv/projekt
http://linked.open...UplatneniVysledku
http://linked.open...iv/tvurceVysledku
  • Strejček, Jan
  • Křetínský, Mojmír
  • Blahoudek, František
  • Duret-Lutz, Alexandre
http://linked.open...vavai/riv/typAkce
http://linked.open.../riv/zahajeniAkce
number of pages
http://bibframe.org/vocab/doi
  • 10.1145/2632362.2632377
http://purl.org/ne...btex#hasPublisher
  • ACM
https://schema.org/isbn
  • 9781450324526
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