Token Games and History-Deterministic Quantitative-Automata
A nondeterministic automaton is history-deterministic if its nondeterminism can be resolved by only considering the prefix of the word read so far. Due to their good compositional properties, history-deterministic automata are useful in solving games and synthesis problems. Deciding whether a given...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2023-11-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/9922/pdf |
| _version_ | 1797268515490627584 |
|---|---|
| author | Udi Boker Karoliina Lehtinen |
| author_facet | Udi Boker Karoliina Lehtinen |
| author_sort | Udi Boker |
| collection | DOAJ |
| description | A nondeterministic automaton is history-deterministic if its nondeterminism
can be resolved by only considering the prefix of the word read so far. Due to
their good compositional properties, history-deterministic automata are useful
in solving games and synthesis problems. Deciding whether a given
nondeterministic automaton is history-deterministic (the HDness problem) is
generally a difficult task, which can involve an exponential procedure, or even
be undecidable, as is the case for example with pushdown automata. Token games
provide a PTime solution to the HDness problem of B\"uchi and coB\"uchi
automata, and it is conjectured that 2-token games characterise HDness for all
$\omega$-regular automata.
We extend token games to the quantitative setting and analyse their potential
to help deciding HDness of quantitative automata. In particular, we show that
1-token games characterise HDness for all quantitative (and Boolean) automata
on finite words, as well as discounted-sum (DSum), Inf and Reachability
automata on infinite words, and that 2-token games characterise HDness of
LimInf and LimSup automata, as well as Sup automata on infinite words. Using
these characterisations, we provide solutions to the HDness problem of Safety,
Reachability, Inf and Sup automata on finite and infinite words in PTime, of
DSum automata on finite and infinite words in NP$\cap$co-NP, of LimSup automata
in quasipolynomial time, and of LimInf automata in exponential time, where the
latter two are only polynomial for automata with a logarithmic number of
weights. |
| first_indexed | 2024-04-25T01:33:42Z |
| format | Article |
| id | doaj.art-b50ddae343d74b6ca62594ebc750346c |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:33:42Z |
| publishDate | 2023-11-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-b50ddae343d74b6ca62594ebc750346c2024-03-08T10:43:58ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742023-11-01Volume 19, Issue 410.46298/lmcs-19(4:8)20239922Token Games and History-Deterministic Quantitative-AutomataUdi BokerKaroliina LehtinenA nondeterministic automaton is history-deterministic if its nondeterminism can be resolved by only considering the prefix of the word read so far. Due to their good compositional properties, history-deterministic automata are useful in solving games and synthesis problems. Deciding whether a given nondeterministic automaton is history-deterministic (the HDness problem) is generally a difficult task, which can involve an exponential procedure, or even be undecidable, as is the case for example with pushdown automata. Token games provide a PTime solution to the HDness problem of B\"uchi and coB\"uchi automata, and it is conjectured that 2-token games characterise HDness for all $\omega$-regular automata. We extend token games to the quantitative setting and analyse their potential to help deciding HDness of quantitative automata. In particular, we show that 1-token games characterise HDness for all quantitative (and Boolean) automata on finite words, as well as discounted-sum (DSum), Inf and Reachability automata on infinite words, and that 2-token games characterise HDness of LimInf and LimSup automata, as well as Sup automata on infinite words. Using these characterisations, we provide solutions to the HDness problem of Safety, Reachability, Inf and Sup automata on finite and infinite words in PTime, of DSum automata on finite and infinite words in NP$\cap$co-NP, of LimSup automata in quasipolynomial time, and of LimInf automata in exponential time, where the latter two are only polynomial for automata with a logarithmic number of weights.https://lmcs.episciences.org/9922/pdfcomputer science - formal languages and automata theory |
| spellingShingle | Udi Boker Karoliina Lehtinen Token Games and History-Deterministic Quantitative-Automata Logical Methods in Computer Science computer science - formal languages and automata theory |
| title | Token Games and History-Deterministic Quantitative-Automata |
| title_full | Token Games and History-Deterministic Quantitative-Automata |
| title_fullStr | Token Games and History-Deterministic Quantitative-Automata |
| title_full_unstemmed | Token Games and History-Deterministic Quantitative-Automata |
| title_short | Token Games and History-Deterministic Quantitative-Automata |
| title_sort | token games and history deterministic quantitative automata |
| topic | computer science - formal languages and automata theory |
| url | https://lmcs.episciences.org/9922/pdf |
| work_keys_str_mv | AT udiboker tokengamesandhistorydeterministicquantitativeautomata AT karoliinalehtinen tokengamesandhistorydeterministicquantitativeautomata |