Deeper Connections between LTL and Alternating Automata

PELÁNEK, Radek and Jan STREJČEK. Deeper Connections between LTL and Alternating Automata. In Implementation and Application of Automata. Berlin, Heidelberg: Springer-Verlag, 2005, p. 238-249. ISBN 978-3-540-31023-5.

Basic information

Original name

Deeper Connections between LTL and Alternating Automata

Name in Czech

Hlubší spojitosti mezi LTL a alternujícími automaty

Authors

PELÁNEK, Radek (203 Czech Republic) and Jan STREJČEK (203 Czech Republic, guarantor)

Edition

Berlin, Heidelberg, Implementation and Application of Automata, p. 238-249, 12 pp. 2005

Publisher

Springer-Verlag

---

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

France

Confidentiality degree

není předmětem státního či obchodního tajemství

RIV identification code

RIV/00216224:14330/05:00012729

Organization unit

Faculty of Informatics

ISBN

978-3-540-31023-5

UT WoS

000236480300020

Keywords in English

LTL; alternating automata; model checking

Tags

alternating automata, LTL, Model checking

Tags

International impact, Reviewed

---

Abstract

V originále

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.

In Czech

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ů.

---

Links

GA201/03/0509, research and development project	Name: Automatizovaná verifikace paralelních a distribuovaných systémů Investor: Czech Science Foundation, Automated Verification of Parallel and Distributed Systems
GD102/05/H050, research and development project	Name: Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů Investor: Czech Science Foundation, Integrated approach to education of PhD students in the area of parallel and distributed systems
MSM0021622419, plan (intention)	Name: Vysoce paralelní a distribuované výpočetní systémy Investor: Ministry of Education, Youth and Sports of the CR, Highly Parallel and Distributed Computing Systems
1M0545, research and development project	Name: Institut Teoretické Informatiky Investor: Ministry of Education, Youth and Sports of the CR, Institute for Theoretical Computer Science