About: Compositional Approach to Suspension and Other Improvements to LTL Translation     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
  • Recently, there was defined a fragment of LTL (containing fairness properties among other interesting formulae) whose validity over a given infinite word depends only on an arbitrary suffix of the word. Building upon an existing translation from LTL to Büchi automata, we introduce a compositional approach where subformulae of this fragment are translated separately from the rest of an input formula and the produced automata are composed in a way that the subformulae are checked only in relevant accepting strongly connected components of the final automaton. Further, we suggest improvements over some procedures commonly applied to generalized Büchi automata, namely over generalized acceptance simplification and over degeneralization. Finally we show how existing simulation-based reductions can be implemented in a signature-based framework in a way that improves the determinism of the automaton.
  • Recently, there was defined a fragment of LTL (containing fairness properties among other interesting formulae) whose validity over a given infinite word depends only on an arbitrary suffix of the word. Building upon an existing translation from LTL to Büchi automata, we introduce a compositional approach where subformulae of this fragment are translated separately from the rest of an input formula and the produced automata are composed in a way that the subformulae are checked only in relevant accepting strongly connected components of the final automaton. Further, we suggest improvements over some procedures commonly applied to generalized Büchi automata, namely over generalized acceptance simplification and over degeneralization. Finally we show how existing simulation-based reductions can be implemented in a signature-based framework in a way that improves the determinism of the automaton. (en)
Title
  • Compositional Approach to Suspension and Other Improvements to LTL Translation
  • Compositional Approach to Suspension and Other Improvements to LTL Translation (en)
skos:prefLabel
  • Compositional Approach to Suspension and Other Improvements to LTL Translation
  • Compositional Approach to Suspension and Other Improvements to LTL Translation (en)
skos:notation
  • RIV/00216224:14330/13:00066141!RIV14-MSM-14330___
http://linked.open...avai/riv/aktivita
http://linked.open...avai/riv/aktivity
  • 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
  • 66524
http://linked.open...ai/riv/idVysledku
  • RIV/00216224:14330/13:00066141
http://linked.open...riv/jazykVysledku
http://linked.open.../riv/klicovaSlova
  • linear time logic; model-checking; translation LTL to Buchi automata (en)
http://linked.open.../riv/klicoveSlovo
http://linked.open...ontrolniKodProRIV
  • [229A1FCEAF0E]
http://linked.open...v/mistoKonaniAkce
  • Stony Brook, NY, USA
http://linked.open...i/riv/mistoVydani
  • Berlin Heidelberg
http://linked.open...i/riv/nazevZdroje
  • Model Checking Software - 20th International Symposium, SPIN 2013
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
  • Babiak, Tomáš
  • Strejček, Jan
  • Křetínský, Mojmír
  • Badie, Thomas
  • Duret-Lutz, Alexandre
http://linked.open...vavai/riv/typAkce
http://linked.open.../riv/zahajeniAkce
issn
  • 0302-9743
number of pages
http://bibframe.org/vocab/doi
  • 10.1007/978-3-642-39176-7_6
http://purl.org/ne...btex#hasPublisher
  • Springer-Verlag
https://schema.org/isbn
  • 9783642391750
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