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

• Original language: English
• Type of outcome: Proceedings paper
• Field of Study: 10201 Computer sciences, information science, bioinformatics
• Country of publisher: France
• Confidentiality degree: is not subject to a state or trade secret
• 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

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.

Abstract (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