arXiv subjects

A. V. Sreejith

Publications and source records attributed to A. V. Sreejith.

9 recordsLinked to original sources

arXiv2025

Scalable Learning of One-Counter Automata via State-Merging Algorithms

We propose One-counter Positive Negative Inference (OPNI), a passive learning algorithm for deterministic real-time one-counter automata (DROCA). Inspired by the RPNI algorithm for regular languages, OPNI constructs a DROCA consistent with any given valid sample set. We further present a method for combining OPNI with active learning of DROCA, and provide an implementation of the approach. Our experimental results demonstrate that this approach scales more effectively than existing state-of-the-art algorithms. We also evaluate the performance of the proposed approach for learning visibly one-counter automata.

cs.FL↗

arXiv2025

Learning real-time one-counter automata using polynomially many queries

In this paper, we introduce a novel method for active learning of deterministic real-time one-counter automata (DROCA). The existing techniques for learning DROCA rely on observing the behaviour of the DROCA up to exponentially large counter-values. Our algorithm eliminates this need and requires only a polynomial number of queries. Additionally, our method differs from existing techniques as we learn a minimal counter-synchronous DROCA, resulting in much smaller counter-examples on equivalence queries. Learning a minimal counter-synchronous DROCA cannot be done in polynomial time unless P = NP, even in the case of visibly one-counter automata. We use a SAT solver to overcome this difficulty. The solver is used to compute a minimal separating DFA from a given set of positive and negative samples. We prove that the equivalence of two counter-synchronous DROCAs can be checked significantly faster than that of general DROCAs. For visibly one-counter automata, we have discovered an even faster algorithm for equivalence checking. We implemented the proposed learning algorithm and tested it on randomly generated DROCAs. Our evaluations show that the proposed method outperforms the existing techniques on the test set.

cs.FL↗

arXiv2025

Learning Deterministic One-Counter Automata in Polynomial Time

We give an active learning algorithm for deterministic one-counter automata (DOCAs) where the learner can ask the teacher membership and minimal equivalence queries. The algorithm called OL* learns a DOCA in time polynomial in the size of the smallest DOCA, recognising the target language. All existing algorithms for learning DOCAs, even for the subclasses of deterministic real-time one-counter automata (DROCAs) and visibly one-counter automata (VOCAs), in the worst case, run in exponential time with respect to the size of the DOCA under learning. Furthermore, previous learning algorithms are ``grey-box'' algorithms relying on an additional query type - counter value query - where the teacher returns the counter value reached on reading a given word. In contrast, our algorithm is a ``black-box'' algorithm. It is known that the minimisation of VOCAs is NP-hard. However, OL* can be used for approximate minimisation of DOCAs. In this case, the output size is at most polynomial in the size of a minimal DOCA.

cs.FL↗

arXiv2025

Modulo quantifiers over functional vocabularies extending addition

We show that first order logic (FO) and first order logic extended with modulo counting quantifiers (FOMOD) over purely functional vocabularies which extend addition, satisfy the Crane beach property (CBP) if the logic satisfies a normal form (called positional normal form). This not only shows why logics over the addition vocabulary have the CBP but also gives new CBP results, for example for the vocabulary which extends addition with the exponentiation function. The above results can also be viewed from the perspective of circuit complexity. Showing the existence of regular languages not definable in FOMOD[<, +, *] is equivalent to the separation of the circuit complexity classes ACC0 and NC1 . Our theorem shows that a weaker logic , namely, FOMOD[<,+,2^x] cannot define all regular languages.

cs.LO↗

arXiv2024

Equivalence of Deterministic Weighted Real-time One-Counter Automata

This paper introduces deterministic weighted real-time one-counter automaton (DWROCA). A DWROCA is a deterministic real-time one-counter automaton whose transitions are assigned a weight from a field. Two DWROCAs are equivalent if every word accepted by one is accepted by the other with the same weight. DWROCA is a sub-class of weighted one-counter automata with counter-determinacy. It is known that the equivalence problem for this model is in P. This paper gives a simpler proof and a better polynomial-time algorithm for checking the equivalence of two DWROCAs.

cs.FL↗

arXiv2023

Weighted One-Deterministic-Counter Automata

We introduce weighted one-deterministic-counter automata (ODCA). These are weighted one-counter automata (OCA) with the property of counter-determinacy, meaning that all paths labelled by a given word starting from the initial configuration have the same counter-effect. Weighted ODCAs are a strict extension of weighted visibly OCAs, which are weighted OCAs where the input alphabet determines the actions on the counter. We present a novel problem called the co-VS (complement to a vector space) reachability problem for weighted ODCAs over fields, which seeks to determine if there exists a run from a given configuration of a weighted ODCA to another configuration whose weight vector lies outside a given vector space. We establish two significant properties of witnesses for co-VS reachability: they satisfy a pseudo-pumping lemma, and the lexicographically minimal witness has a special form. It follows that the co-VS reachability problem is in P. These reachability problems help us to show that the equivalence problem of weighted ODCAs over fields is in P by adapting the equivalence proof of deterministic real-time OCAs by Böhm et al. This is a step towards resolving the open question of the equivalence problem of weighted OCAs. Furthermore, we demonstrate that the regularity problem, the problem of checking whether an input weighted ODCA over a field is equivalent to some weighted automaton, is in P. Finally, we show that the covering and coverable equivalence problems for uninitialised weighted ODCAs are decidable in polynomial time. We also consider boolean ODCAs and show that the equivalence problem for (non-deterministic) boolean ODCAs is in PSPACE, whereas it is undecidable for (non-deterministic) boolean OCAs.

cs.FL↗

arXiv2021

First-Order logic and its Infinitary Quantifier Extensions over Countable Words

We contribute to the refined understanding of the language-logic-algebra interplay in the context of first-order properties of countable words. We establish decidable algebraic characterizations of one variable fragment of FO as well as boolean closure of existential fragment of FO via a strengthening of Simon's theorem about piecewise testable languages. We propose a new extension of FO which admits infinitary quantifiers to reason about the inherent infinitary properties of countable words. We provide a very natural and hierarchical block-product based characterization of the new extension. We also explicate its role in view of other natural and classical logical systems such as WMSO and FO[cut] - an extension of FO where quantification over Dedekind-cuts is allowed. We also rule out the possibility of a finite basis for a block-product based characterization of these logical systems. Finally, we report simple but novel algebraic characterizations of one variable fragments of the hierarchies of the new proposed extension of FO.

cs.LO↗

arXiv2020

Undecidability of a weak version of MSO+U

We prove the undecidability of MSO on $ω$-words extended with the second-order predicate $U_1(X)$ which says that the distance between consecutive positions in a set $X \subseteq \mathbb{N}$ is unbounded. This is achieved by showing that adding $U_1$ to MSO gives a logic with the same expressive power as $MSO+U$, a logic on $ω$-words with undecidable satisfiability. As a corollary, we prove that MSO on $ω$-words becomes undecidable if allowing to quantify over sets of positions that are ultimately periodic, i.e., sets $X$ such that for some positive integer $p$, ultimately either both or none of positions $x$ and $x+p$ belong to $X$.

cs.LO↗

arXiv2012

Non-definability of languages by generalized first-order formulas over (N,+)

We consider first-order logic with monoidal quantifiers over words. We show that all languages with a neutral letter, definable using the addition numerical predicate are also definable with the order predicate as the only numerical predicate. Let S be a subset of monoids. Let LS be the logic closed under quantification over the monoids in S and N be the class of neutral letter languages. Then we show that: LS[<,+] cap N = LS[<] Our result can be interpreted as the Crane Beach conjecture to hold for the logic LS[<,+]. As a corollary of our result we get the result of Roy and Straubing that FO+MOD[<,+] collapses to FO+MOD[<]. For cyclic groups, we answer an open question of Roy and Straubing, proving that MOD[<,+] collapses to MOD[<]. Our result also shows that multiplication is necessary for Barrington's theorem to hold. All these results can be viewed as separation results for very uniform circuit classes. For example we separate FO[<,+]-uniform CC0 from FO[<,+]-uniform ACC0.

cs.LO↗