More Like this

1. Alternating Good-for-MDPs Automata

   https://doi.org/10.1007/978-3-031-19992-9_19  

   Hahn, Ernst Moritz ; Perez, Mateo ; Schewe, Sven ; Somenzi, Fabio ; Trivedi, Ashutosh ; Wojtczak, Dominik ( October 2022 , International Symposium on Automated Technology for Verification and Analysis (ATVA 2022))

   Bouajjani, A. ; Holík, L. ; Wu, Z. (Ed.)

   When omega-regular objectives were first proposed in model-free reinforcement learning (RL) for controlling MDPs, deterministic Rabin automata were used in an attempt to provide a direct translation from their transitions to scalar values. While these translations failed, it has turned out that it is possible to repair them by using good-for-MDPs (GFM) Buechi automata instead. These are nondeterministic Buechi automata with a restricted type of nondeterminism, albeit not as restricted as in good-for-games automata. Indeed, deterministic Rabin automata have a pretty straightforward translation to such GFM automata, which is bi-linear in the number of states and pairs. Interestingly, the same cannot be said for deterministic Streett automata: a translation to nondeterministic Rabin or Buechi automata comes at an exponential cost, even without requiring the target automaton to be good-for-MDPs. Do we have to pay more than that to obtain a good-for-MDPs automaton? The surprising answer is that we have to pay significantly less when we instead expand the good-for-MDPs property to alternating automata: like the nondeterministic GFM automata obtained from deterministic Rabin automata, the alternating good-for-MDPs automata we produce from deterministic Streett automata are bi-linear in the size of the deterministic automaton and its index. They can therefore be exponentially more succinct than the minimal nondeterministic Buechi automaton. 

   more » « less
2. Divide-and-Conquer Determinization of Büchi Automata Based on SCC Decomposition

   Yong Li, Andrea Turrini ( August 2022 , Book cover Book cover International Conference on Computer Aided Verification)

   The determinization of a nondeterministic Büchi automaton (NBA) is a fundamental construction of automata theory, with applications to probabilistic verification and reactive synthesis. The standard determinization constructions, such as the ones based on the Safra-Piterman’s approach, work on the whole NBA. In this work we propose a divide-and-conquer determinization approach. To this end, we first classify the strongly connected components (SCCs) of the given NBA as inherently weak, deterministic accepting, and nondeterministic accepting. We then present how to determinize each type of SCC independently from the others; this results in an easier handling of the determinization algorithm that takes advantage of the structure of that SCC. Once all SCCs have been determinized, we show how to compose them so to obtain the final equivalent deterministic Emerson-Lei automaton, which can be converted into a deterministic Rabin automaton without blow-up of states and transitions. We implement our algorithm in our tool COLA and empirically evaluate COLA with the state-of-the-art tools Spot and Owl on a large set of benchmarks from the literature. The experimental results show that our prototype COLA outperforms Spot and Owl regarding the number of states and transitions. 

   more » « less
3. Asynchronous Automata Processing on GPUs

   https://doi.org/10.1145/3579453  

   Liu, Hongyuan ; Pai, Sreepathi ; Jog, Adwait ( February 2023 , Proceedings of the ACM on Measurement and Analysis of Computing Systems)

   Finite-state automata serve as compute kernels for many application domains such as pattern matching and data analytics. Existing approaches on GPUs exploit three levels of parallelism in automata processing tasks: 1)~input stream level, 2)~automaton-level and 3)~state-level. Among these, only state-level parallelism is intrinsic to automata while the other two levels of parallelism depend on the number of automata and input streams to be processed. As GPU resources increase, a parallelism-limited automata processing task can underutilize GPU compute resources. To this end, we propose AsyncAP, a low-overhead approach that optimizes for both scalability and throughput. Our insight is that most automata processing tasks have an additional source of parallelism originating from the input symbols which has not been leveraged before. Making the matching process associated with the automata tasks asynchronous, i.e., parallel GPU threads start processing an input stream from different input locations instead of processing it serially, improves throughput significantly, and scales with input length. When the task does not have enough parallelism to utilize all the GPU cores, detailed evaluation across 12 evaluated applications shows that AsyncAP achieves up to 58× speedup on average over the state-of-the-art GPU automata processing engine. When the tasks have enough parallelism to utilize GPU cores, AsyncAP still achieves 2.4× speedup. 

   more » « less
4. Depth-First Search in Directed Graphs, Revisited

   Allender, Eric ; Chauhan, Archit ; Datta, Samir ( January 2020 , Electronic colloquium on computational complexity)

   We present an algorithm for constructing a depth-first search tree in planar digraphs; the algorithm can be implemented in the complexity class UL, which is contained in nondeterministic logspace NL, which in turn lies in NC^2. Pior to this (for more than a quarter-century), the fastest uniform deterministic parallel algorithm for this problem was O(log^10 n) (corresponding to the complexity class AC^10 ⊆ NC^11). We also consider the problem of computing depth-first search trees in other classes of graphs, and obtain additional new upper bounds. 

   more » « less
5. Good-for-MDPs Automata for Probabilistic Analysis and Reinforcement Learning

   https://doi.org/10.1007/978-3-030-45190-5_17  

   Hahn, E. M. ; Perez, Mateo ; Schewe, Sven ; Somenzi, Fabio ; Trivedi, Ashutosh ; and Wojtczak, Dominik ( April 2020 , Tools and Algorithms for the Construction and Analysis of Systems)

   Biere, Armin ; Parker, David (Ed.)

   We characterize the class of nondeterministic 𝜔-automata that can be used for the analysis of finite Markov decision processes (MDPs). We call these automata ‘good-for-MDPs’ (GFM). We show that GFM automata are closed under classic simulation as well as under more powerful simulation relations that leverage properties of optimal control strategies for MDPs. This closure enables us to exploit state-space reduction techniques, such as those based on direct and delayed simulation, that guarantee simulation equivalence. We demonstrate the promise of GFM automata by defining a new class of automata with favorable properties—they are Büchi automata with low branching degree obtained through a simple construction—and show that going beyond limit-deterministic automata may significantly benefit reinforcement learning. 

   more » « less