From Nondeterministic B\"uchi and Streett Automata to Deterministic Parity Automata
In this paper we revisit Safra's determinization constructions for automata on infinite words. We show how to construct deterministic automata with fewer states and, most importantly, parity acceptance conditions. Determinization is used in numerous applications, such as reasoning about tree au...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2007-08-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/1199/pdf |
| _version_ | 1797268772103389184 |
|---|---|
| author | Nir Piterman |
| author_facet | Nir Piterman |
| author_sort | Nir Piterman |
| collection | DOAJ |
| description | In this paper we revisit Safra's determinization constructions for automata
on infinite words. We show how to construct deterministic automata with fewer
states and, most importantly, parity acceptance conditions. Determinization is
used in numerous applications, such as reasoning about tree automata,
satisfiability of CTL*, and realizability and synthesis of logical
specifications. The upper bounds for all these applications are reduced by
using the smaller deterministic automata produced by our construction. In
addition, the parity acceptance conditions allows to use more efficient
algorithms (when compared to handling Rabin or Streett acceptance conditions). |
| first_indexed | 2024-04-25T01:37:47Z |
| format | Article |
| id | doaj.art-7a6f80467e554699aeed5aca56dcdaa7 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:37:47Z |
| publishDate | 2007-08-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-7a6f80467e554699aeed5aca56dcdaa72024-03-08T08:48:26ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742007-08-01Volume 3, Issue 310.2168/LMCS-3(3:5)20071199From Nondeterministic B\"uchi and Streett Automata to Deterministic Parity AutomataNir Pitermanhttps://orcid.org/0000-0002-8242-5357In this paper we revisit Safra's determinization constructions for automata on infinite words. We show how to construct deterministic automata with fewer states and, most importantly, parity acceptance conditions. Determinization is used in numerous applications, such as reasoning about tree automata, satisfiability of CTL*, and realizability and synthesis of logical specifications. The upper bounds for all these applications are reduced by using the smaller deterministic automata produced by our construction. In addition, the parity acceptance conditions allows to use more efficient algorithms (when compared to handling Rabin or Streett acceptance conditions).https://lmcs.episciences.org/1199/pdfcomputer science - logic in computer sciencecomputer science - formal languages and automata theoryf.1.1f.4.3 |
| spellingShingle | Nir Piterman From Nondeterministic B\"uchi and Streett Automata to Deterministic Parity Automata Logical Methods in Computer Science computer science - logic in computer science computer science - formal languages and automata theory f.1.1 f.4.3 |
| title | From Nondeterministic B\"uchi and Streett Automata to Deterministic Parity Automata |
| title_full | From Nondeterministic B\"uchi and Streett Automata to Deterministic Parity Automata |
| title_fullStr | From Nondeterministic B\"uchi and Streett Automata to Deterministic Parity Automata |
| title_full_unstemmed | From Nondeterministic B\"uchi and Streett Automata to Deterministic Parity Automata |
| title_short | From Nondeterministic B\"uchi and Streett Automata to Deterministic Parity Automata |
| title_sort | from nondeterministic b uchi and streett automata to deterministic parity automata |
| topic | computer science - logic in computer science computer science - formal languages and automata theory f.1.1 f.4.3 |
| url | https://lmcs.episciences.org/1199/pdf |
| work_keys_str_mv | AT nirpiterman fromnondeterministicbuchiandstreettautomatatodeterministicparityautomata |