About: LTL to Büchi Automata Translation: Fast and More Deterministic

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

About: LTL to Büchi Automata Translation: Fast and More Deterministic 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	We introduce improvements in the algorithm by Gastin and Oddoux translating LTL formulae into Büchi automata via very weak alternating co-Büchi automata and generalized Büchi automata. Several improvements are based on specific properties of any formula where each branch of its syntax tree contains at least one eventually operator and at least one always operator. These changes usually result in faster translations and smaller automata. Other improvements reduce non-determinism in the produced automata. In fact, we modified all the steps of the original algorithm and its implementation known as LTL2BA. Experimental results show that our modifications are real improvements. Their implementations within an LTL2BA translation made LTL2BA very competitive with the current version of SPOT, sometimes outperforming it substantially. We introduce improvements in the algorithm by Gastin and Oddoux translating LTL formulae into Büchi automata via very weak alternating co-Büchi automata and generalized Büchi automata. Several improvements are based on specific properties of any formula where each branch of its syntax tree contains at least one eventually operator and at least one always operator. These changes usually result in faster translations and smaller automata. Other improvements reduce non-determinism in the produced automata. In fact, we modified all the steps of the original algorithm and its implementation known as LTL2BA. Experimental results show that our modifications are real improvements. Their implementations within an LTL2BA translation made LTL2BA very competitive with the current version of SPOT, sometimes outperforming it substantially. (en)
Title	LTL to Büchi Automata Translation: Fast and More Deterministic LTL to Büchi Automata Translation: Fast and More Deterministic (en)
skos:prefLabel	LTL to Büchi Automata Translation: Fast and More Deterministic LTL to Büchi Automata Translation: Fast and More Deterministic (en)
skos:notation	RIV/00216224:14330/12:00057222!RIV13-GA0-14330___
http://linked.open...avai/predkladatel	Fakulta informatiky
http://linked.open...avai/riv/aktivita	P S Z
http://linked.open...avai/riv/aktivity	P(GA201/09/1389), P(GAP202/10/1469), P(GBP202/12/G061), P(GD102/09/H042), P(GPP202/12/P612), S, Z(MSM0021622419)
http://linked.open...vai/riv/dodaniDat	2013
http://linked.open...aciTvurceVysledku	Řehák, Vojtěch Strejček, Jan Babiak, Tomáš Křetínský, Mojmír
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	147549
http://linked.open...ai/riv/idVysledku	RIV/00216224:14330/12:00057222
http://linked.open...riv/jazykVysledku	eng - angličtina
http://linked.open.../riv/klicovaSlova	Linear Temporal Logic; Büchi Automata (en)
http://linked.open.../riv/klicoveSlovo	Büchi Automata Linear Temporal Logic
http://linked.open...ontrolniKodProRIV	[0DFE4B76434F]
http://linked.open...v/mistoKonaniAkce	Tallinn, Estonia
http://linked.open...i/riv/mistoVydani	Berlin, Heidelberg
http://linked.open...i/riv/nazevZdroje	TACAS 2012: 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems
http://linked.open...in/vavai/riv/obor	IN
http://linked.open...ichTvurcuVysledku	4 (xsd:int)
http://linked.open...cetTvurcuVysledku	4 (xsd:int)
http://linked.open...vavai/riv/projekt	Formal methods for analysis and verification of complex systems Center of excellence - Institute for theoretical computer science (CE-ITI) Verification and Analysis of Large-Scale Computer Systems Mathematical and Engineering Approaches to Developing Reliable and Secure Concurrent and Distributed Computer Systems Formální verifikace stochastických systémů s reálným časem
http://linked.open...UplatneniVysledku	2012
http://linked.open...iv/tvurceVysledku	Řehák, Vojtěch Babiak, Tomáš Strejček, Jan Křetínský, Mojmír
http://linked.open...vavai/riv/typAkce	WRD - Světová
http://linked.open.../riv/zahajeniAkce	2012-01-01 (xsd:date)
http://linked.open...n/vavai/riv/zamer	Highly Parallel and Distributed Computing Systems
issn	0302-9743
number of pages	15 (xsd:int)
http://bibframe.org/vocab/doi	10.1007/978-3-642-28756-5_8
http://purl.org/ne...btex#hasPublisher	Springer-Verlag
https://schema.org/isbn	9783642287558
http://localhost/t...ganizacniJednotka	14330
is http://linked.open...avai/riv/vysledek of	LTL to Büchi Automata Translation: Fast and More Deterministic

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