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. |
Other formats:
BibTeX
LaTeX
RIS
|
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 |
Changed by | Changed by: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Changed: 29/3/2010 12:50. |
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 |
PrintDisplayed: 3/10/2024 08:22