More Like this

1. Toward Determining NFA Equivalence via QBFs (Student Abstract)

   Miller, H; Narvaez, D (January 2021, Thirty-Fifth AAAI Conference on Artificial Intelligence)

   null (Ed.)

   Equivalence of deterministic finite automata (DFAs) has been researched for several decades, but equivalence of nondeterministic finite automata (NFAs) is not as studied. Equivalence of two NFAs is a PSPACE-complete problem. NFA equivalence is a challenging theoretical problem with practical applications such as lexical analysis. Quantified boolean formulas (QBFs) naturally encode PSPACE-complete problems, and we share our preliminary work towards determining NFA equivalence via QBFs. 

   more » « less
2. Hybrid Compositional Reasoning for Reactive Synthesis from Finite-Horizon Specifications.

   Bansal, Suguman (April 2020, Proceedings of the AAAI Conference on Artificial Intelligence)

   LTLf synthesis is the automated construction of a reactive system from a high-level description, expressed in LTLf, of its finite-horizon behavior. So far, the conversion of LTLf formulas to deterministic finite-state automata (DFAs) has been identified as the primary bottleneck to the scalabity of synthesis. Recent investigations have also shown that the size of the DFA state space plays a critical role in synthesis as well. Therefore, effective resolution of the bottleneck for synthesis requires the conversion to be time and memory performant, and prevent state-space explosion. Current conversion approaches, however, which are based either on explicit-state representation or symbolic-state representation, fail to address these necessities adequately at scale: Explicit-state approaches generate minimal DFA but are slow due to expensive DFA minimization. Symbolic-state representations can be succinct, but due to the lack of DFA minimization they generate such large state spaces that even their symbolic representations cannot compensate for the blow-up. This work proposes a hybrid representation approach for the conversion. Our approach utilizes both explicit and symbolic representations of the state-space, and effectively leverages their complementary strengths. In doing so, we offer an LTLf to DFA conversion technique that addresses all three necessities, hence resolving the bottleneck. A comprehensive empirical evaluation on conversion and synthesis benchmarks supports the merits of our hybrid approach. 

   more » « less
3. Hybrid Compositional Reasoning for Reactive Synthesis from Finite-Horizon Specifications

   https://doi.org/10.1609/aaai.v34i06.6528  

   Bansal, Suguman; Li, Yong; Tabajara, Lucas; Vardi, Moshe (June 2020, Proceedings of the AAAI Conference on Artificial Intelligence)

   LTLf synthesis is the automated construction of a reactive system from a high-level description, expressed in LTLf, of its finite-horizon behavior. So far, the conversion of LTLf formulas to deterministic finite-state automata (DFAs) has been identified as the primary bottleneck to the scalabity of synthesis. Recent investigations have also shown that the size of the DFA state space plays a critical role in synthesis as well.Therefore, effective resolution of the bottleneck for synthesis requires the conversion to be time and memory performant, and prevent state-space explosion. Current conversion approaches, however, which are based either on explicit-state representation or symbolic-state representation, fail to address these necessities adequately at scale: Explicit-state approaches generate minimal DFA but are slow due to expensive DFA minimization. Symbolic-state representations can be succinct, but due to the lack of DFA minimization they generate such large state spaces that even their symbolic representations cannot compensate for the blow-up.This work proposes a hybrid representation approach for the conversion. Our approach utilizes both explicit and symbolic representations of the state-space, and effectively leverages their complementary strengths. In doing so, we offer an LTLf to DFA conversion technique that addresses all three necessities, hence resolving the bottleneck. A comprehensive empirical evaluation on conversion and synthesis benchmarks supports the merits of our hybrid approach. 

   more » « less
4. The Complexity of Iterated Reversible Computation

   https://doi.org/10.46298/theoretics.23.10  

   Eppstein, David (December 2023, TheoretiCS)

   We study a class of functional problems reducible to computing $$f^{(n)}(x)$$for inputs $$n$$ and $$x$$, where $$f$$ is a polynomial-time bijection. As we prove,the definition is robust against variations in the type of reduction used inits definition, and in whether we require $$f$$ to have a polynomial-time inverseor to be computible by a reversible logic circuit. These problems arecharacterized by the complexity class $$\mathsf{FP}^{\mathsf{PSPACE}}$$, andinclude natural $$\mathsf{FP}^{\mathsf{PSPACE}}$$-complete problems in circuitcomplexity, cellular automata, graph algorithms, and the dynamical systemsdescribed by piecewise-linear transformations. 

   more » « less
5. Finite State Mean Field Games with Major and Minor Players

   Rene Carmona, Peiqi Wang (July 2018, arXiv.org)

   The goal of the paper is to develop the theory of finite state mean field games with major and minor players when the state space of the game is finite. We introduce the finite player games and derive a mean field game formulation in the limit when the number of minor players tends to infinity. In this limit, we prove that the value functions of the optimization problems are viscosity solutions of PIDEs of the HJB type, and we construct the best responses for both types of players. From there, we prove existence of Nash equilibria under reasonable assumptions. Finally we prove that a form of propagation of chaos holds in the present context and use this result to prove existence of approximate Nash equilibria for the finite player games from the solutions of the mean field games. this vindicate our formulation of the mean field game problem. 

   more » « less