Deeper Connections between LTL and Alternating Automata
PELÁNEK, Radek a Jan STREJČEK. Deeper Connections between LTL and Alternating Automata. In Implementation and Application of Automata. Berlin, Heidelberg: Springer-Verlag, 2005, s. 238-249. ISBN 978-3-540-31023-5. |
Další formáty:
BibTeX
LaTeX
RIS
|
Základní údaje | |
---|---|
Originální název | Deeper Connections between LTL and Alternating Automata |
Název česky | Hlubší spojitosti mezi LTL a alternujícími automaty |
Autoři | PELÁNEK, Radek (203 Česká republika) a Jan STREJČEK (203 Česká republika, garant). |
Vydání | Berlin, Heidelberg, Implementation and Application of Automata, od s. 238-249, 12 s. 2005. |
Nakladatel | Springer-Verlag |
Další údaje | |
---|---|
Originální jazyk | angličtina |
Typ výsledku | Stať ve sborníku |
Obor | 10201 Computer sciences, information science, bioinformatics |
Stát vydavatele | Francie |
Utajení | není předmětem státního či obchodního tajemství |
Kód RIV | RIV/00216224:14330/05:00012729 |
Organizační jednotka | Fakulta informatiky |
ISBN | 978-3-540-31023-5 |
UT WoS | 000236480300020 |
Klíčová slova anglicky | LTL; alternating automata; model checking |
Štítky | alternating automata, LTL, Model checking |
Příznaky | Mezinárodní význam, Recenzováno |
Změnil | Změnil: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Změněno: 29. 3. 2010 12:50. |
Anotace |
---|
It is known that Linear Temporal Logic (LTL) has the same expressive power as alternating 1-weak automata (A1W automata, also called alternating linear automata or very weak alternating automata). A~translation of LTL formulae into a language equivalent A1W automata has been introduced in [MSS88]. The inverse translation has been developed independently in [Roh97] and [LT00]. In the first part of the paper we show that the latter translation wastes temporal operators and we propose some improvements of this translation. The second part of the paper draws a direct connection between fragments of the Until-Release hierarchy [CP03] and alternation depth of nonaccepting and accepting states in A1W automata. We also indicate some corollaries and applications of these results. |
Anotace česky |
---|
Je známo, že lineární temporální logika (LTL) má stejnou vyjadřovací sílu jako alternujicí 1-weak automaty (A1W automaty, také nazývané lineární automaty nebo velmi slabé automaty). Překlad LTL formulí na jazykově ekvivalentní A1W automat byl popsán v [MSS88]. Opačný překlad byl nezávisle vyvinut v [Roh97] a [LT00]. V první části článku ukazujeme, že druhý převod zbytečně plýtvá temporálními operátory a ukazujeme, jak jej zlepšit. Druhá část článku ukazuje přímou spojitost mezi fragmenty hierarchie Until-Release [CP03] a hloubkou alternace akceptujících a zamítajících stavů v A1W automatu. Na závěr ukazujeme některé důsledky a aplikace těchto výsledků. |
Návaznosti | |
---|---|
GA201/03/0509, projekt VaV | Název: Automatizovaná verifikace paralelních a distribuovaných systémů |
Investor: Grantová agentura ČR, Automatizovaná verifikace paralelních a distribuovaných systémů | |
GD102/05/H050, projekt VaV | Název: Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů |
Investor: Grantová agentura ČR, Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů | |
MSM0021622419, záměr | Název: Vysoce paralelní a distribuované výpočetní systémy |
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy | |
1M0545, projekt VaV | Název: Institut Teoretické Informatiky |
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky |
VytisknoutZobrazeno: 17. 8. 2024 03:44