Sreejith A V / ശ്രീജിത്ത് എ വി

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.

We investigate the expressive power of regular expressions for languages of countable words and establish their expressive equivalence with logical and algebraic characterizations. Our goal is to extend the classical theory of regular languages, defined over finite words and characterized by automata, monadic second-order logic, and regular expressions, to the setting of countable words. In this paper, we introduce and study five classes of expressions: marked star-free expressions, marked expressions, power-free expressions, scatter-free expressions, and scatter expressions. We show that these expression classes characterize natural fragments of logic over countable words and possess decidable algebraic characterizations. As part of our algebraic analysis, we provide a precise description of the relevant classes in terms of their J-class structure. These results complete a triad of equivalences between logic, algebra, and expressions in this richer setting, thereby generalizing foundational results from classical formal language theory.

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.

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.

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.

We contribute to the refined understanding of language-logic-algebra interplay in a recent algebraic framework over countable words. Algebraic characterizations of the one variable fragment of FO as well as the boolean closure of the existential fragment of FO are established. We develop a seamless integration of the block product operation in the countable setting, and generalize well-known decompositional characterizations of FO and its two variable fragment. We propose an extension of FO admitting infinitary quantifiers to reason about inherent infinitary properties of countable words, and obtain a natural hierarchical block-product based characterization of this extension. Properties expressible in this extension can be simultaneously expressed in the classical logical systems such as WMSO and FO[cut]. We also rule out the possibility of a finite-basis for a block-product based characterization of these logical systems. Finally, we report algebraic characterizations of one variable fragments of the hierarchies of the new extension.

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 Bohm 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.

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.

We propose an innovative methodology to estimate the formative discharge of alluvial rivers from remote sensing images. This procedure involves automatic extraction of the width of a channel from Landsat Thematic Mapper, Landsat 8, and Sentinel-1 satellite images. We translate the channel width extracted from satellite images to discharge by using a width-discharge regime curve established previously by us for the Himalayan Rivers. This regime curve is based on the threshold theory, a simple physical force balance that explains the first-order geometry of alluvial channels. Using this procedure, we estimate the discharge of six major rivers of the Himalayan Foreland: the Brahmaputra, Chenab, Ganga, Indus, Kosi, and Teesta rivers. Except highly regulated rivers (Indus and Chenab), our estimates of the discharge from satellite images can be compared with the mean annual discharge obtained from historical records of gauging stations. We have shown that this procedure applies both to braided and single-thread rivers over a large territory. Further, our methodology to estimate discharge from remote sensing images does not rely on continuous ground calibration.

We prove that MSO on omega-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. We obtain it as a corollary of the undecidability of MSO on omega-words extended with the second-order predicate U₁(X) which says that the distance between consecutive positions in a set X subset N is unbounded. This is achieved by showing that adding U₁ to MSO gives a logic with the same expressive power as MSO+U, a logic on omega-words with undecidable satisfiability.

We give the definition of Block Product for finite monoids with generalized associativity.

We propose a seamless integration of the block product operation to the recently developed algebraic framework for regular languages of countable words. A simple but subtle accompanying block product principle has been established. Building on this, we generalize the well-known algebraic characterizations of first-order logic, respectively first-order logic with two variables, in terms of strongly, respectively weakly, iterated block products. We use this to arrive at a complete analogue of Schutzenberger-McNaughton-Papert theorem for countable words. We also explicate the role of block products for linear temporal logic by formulating a novel algebraic characterization of a natural fragment.

Etessami, Vardi and Wilke showed that satisfiability of two-variable first order logic FO²[<] on word models is Nexptime-complete. We extend this upper bound to the slightly stronger logic FO²[<,successor,equiv], which allows checking whether a word position is congruent to r modulo q, for some divisor q and remainder r. If we allow the more powerful modulo counting quantifiers of Straubing, Therien and Thomas, we call this two-variable fragment FOMOD²[<,successor], satisfiability becomes Expspace-complete. A more general counting quantifier, FOCOUNT²[<,successor], makes the logic undecidable.

We study the class of languages of finitely-labelled countable linear orderings definable in two-variable first-order logic. We give a number of characterisations, in particular an algebraic one in terms of circle monoids, using equations. This generalises the corresponding characterisation, namely variety DA, over finite words to the countable case. A corollary is that the membership in this class is decidable: for instance given an MSO formula it is possible to check if there is an equivalent two-variable logic formula over countable linear orderings. In addition, we prove that the satisfiability problems for two-variable logic over arbitrary, countable, and scattered linear orderings are Nexptime-complete.

In this paper, we study several sublogics of monadic second-order logic over countable linear orderings, such as first-order logic, first-order logic on cuts, weak monadic second-order logic, weak monadic second-order logic with cuts, as well as fragments of monadic second-order logic in which sets have to be well ordered or scattered. We give decidable algebraic characterizations of all these logics and compare their respective expressive power.

In this paper we show some lower bounds for the size of multiplicative circuits computing multi-output functions in some noncommutative domains like monoids and finite groups. We also introduce and study a generalization of linear circuits in which the goal is to compute MY where Y is a vector of indeterminates and M is a matrix whose entries come from noncommutative rings. We show some lower bounds in this setting as well.

We consider first-order logic with monoidal quantifiers. 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. Since we prove this result for arbitrary subsets of the monoidal quantifiers, the following holds in the presence of a neutral letter: for aperiodic monoids, we get the result of Libkin that FO[<,+] collapses to FO[<]; for solvable monoids, 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[<]. All these results can be viewed as collapse results for the uniformity of constant depth circuits, and in this sense as a separation result for very uniform circuit classes. For example we separate FO[<,+]-uniform CC⁰ from FO[<,+]-uniform ACC⁰.

Kamp showed that linear temporal logic is expressively complete for first order logic over words. We give a Gabbay style proof to show that linear temporal logic extended with modulo counting and group quantifiers, introduced by Baziramwabo, McKenzie, and Therien, is expressively complete for first order logic with modulo counting, introduced by Straubing, Therien, and Thomas, and group quantifiers, introduced by Barrington, Immerman, and Straubing.

It is well known that modelchecking and satisfiability of Linear Temporal Logic (LTL) are Pspace-complete. Wolper showed that with grammar operators, this result can be extended to increase the expressiveness of the logic to all regular languages. Other ways of extending the expressiveness of LTL using modular and group modalities have been explored by Baziramwabo, McKenzie and Therien, which are expressively complete for regular languages recognized by solvable monoids and for all regular languages, respectively. In all the papers mentioned, the numeric constants used in the modalities are in unary notation. We show that in some cases, such as the modular and symmetric group modalities, we can use numeric constants in binary notation, and still maintain the Pspace upper bound. Adding modulo counting to LTL[F], with just the unary future modality, already makes the logic Pspace-hard. We also consider a restricted logic which allows only the modulo counting of length from the beginning of the word. Its satisfiability is Sigma-three-complete.