About: Almost linear Büchi automata

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

About: Almost linear Büchi automata 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 a new fragment of Linear temporal logic (LTL) called LIO and a new class of Büchi automata (BA) called Almost linear Büchi automata (ALBA). We provide effective translations between LIO and ALBA showing that the two formalisms are expressively equivalent. As we expect applications of our results in model checking, we use two standard sources of specification formulae, namely Spec Patterns and BEEM, to study practical relevance of LIO fragment, and to compare our translation of LIO to ALBA with two standard translations of LTL to BA via alternating automata. Finally, we demonstrate that the LIO to ALBA translation can be much faster than the standard translation and the produced automata can be substantially smaller. We introduce a new fragment of Linear temporal logic (LTL) called LIO and a new class of Büchi automata (BA) called Almost linear Büchi automata (ALBA). We provide effective translations between LIO and ALBA showing that the two formalisms are expressively equivalent. As we expect applications of our results in model checking, we use two standard sources of specification formulae, namely Spec Patterns and BEEM, to study practical relevance of LIO fragment, and to compare our translation of LIO to ALBA with two standard translations of LTL to BA via alternating automata. Finally, we demonstrate that the LIO to ALBA translation can be much faster than the standard translation and the produced automata can be substantially smaller. (en)
Title	Almost linear Büchi automata Almost linear Büchi automata (en)
skos:prefLabel	Almost linear Büchi automata Almost linear Büchi automata (en)
skos:notation	RIV/00216224:14330/12:00057181!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(1M0545), P(GA201/09/1389), P(GAP202/10/1469), P(GD102/09/H042), P(GP201/08/P375), P(GP201/08/P459), S, Z(MSM0021622419)
http://linked.open...iv/cisloPeriodika	2
http://linked.open...vai/riv/dodaniDat	2013
http://linked.open...aciTvurceVysledku	Řehák, Vojtěch Strejček, Jan Babiak, Tomáš
http://linked.open.../riv/druhVysledku	J - Článek v odborném periodiku
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	121713
http://linked.open...ai/riv/idVysledku	RIV/00216224:14330/12:00057181
http://linked.open...riv/jazykVysledku	eng - angličtina
http://linked.open.../riv/klicovaSlova	LTL; linear time logic; model checking (en)
http://linked.open.../riv/klicoveSlovo	LTL linear time logic model checking
http://linked.open...odStatuVydavatele	CZ - Česká republika
http://linked.open...ontrolniKodProRIV	[2C083437627B]
http://linked.open...i/riv/nazevZdroje	Mathematical Structures in Computer Science
http://linked.open...in/vavai/riv/obor	IN
http://linked.open...ichTvurcuVysledku	3 (xsd:int)
http://linked.open...cetTvurcuVysledku	3 (xsd:int)
http://linked.open...vavai/riv/projekt	Formal methods for analysis and verification of complex systems Formal verification: algorithms, properties of modelling formalisms and temporal logics Institute for Theoretical Computer Science Verification and Analysis of Large-Scale Computer Systems Mathematical and Engineering Approaches to Developing Reliable and Secure Concurrent and Distributed Computer Systems New possibilities in automatic verification of network protocols
http://linked.open...UplatneniVysledku	2012
http://linked.open...v/svazekPeriodika	22
http://linked.open...iv/tvurceVysledku	Řehák, Vojtěch Babiak, Tomáš Strejček, Jan
http://linked.open...ain/vavai/riv/wos	000300844900004
http://linked.open...n/vavai/riv/zamer	Highly Parallel and Distributed Computing Systems
issn	0960-1295
number of pages	33 (xsd:int)
http://bibframe.org/vocab/doi	10.1017/S0960129511000399
http://localhost/t...ganizacniJednotka	14330
is http://linked.open...avai/riv/vysledek of	Almost linear Büchi automata

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