Almost linear Büchi automata

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F12%3A00057181" target="_blank" >RIV/00216224:14330/12:00057181 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1017/S0960129511000399" target="_blank" >http://dx.doi.org/10.1017/S0960129511000399</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1017/S0960129511000399" target="_blank" >10.1017/S0960129511000399</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Almost linear Büchi automata

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Almost linear Büchi automata

Popis výsledku anglicky

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.

Druh

J_x - Nezařazeno - Článek v odborném periodiku (Jimp, Jsc a Jost)

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>Z - Vyzkumny zamer (s odkazem do CEZ)<br>S - Specificky vyzkum na vysokych skolach

Rok uplatnění

2012

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název periodika

Mathematical Structures in Computer Science

ISSN

0960-1295

e-ISSN

—

Svazek periodika

22

Číslo periodika v rámci svazku

2

Stát vydavatele periodika

CZ - Česká republika

Počet stran výsledku

33

Strana od-do

203-235

Kód UT WoS článku

000300844900004

EID výsledku v databázi Scopus

—