I am interested in theoretical computer science, especially formal methods.
I did my Bachelor of Technology (B.Tech) from
College of
engineering,Thiruvananthapuram (CET), followed by a Master of Technology (MTech) from
IIT, Madras.
My Ph.D was done under the guidance of Prof.
Kamal Lodaya in
Institute of Mathematical Sciences, Chennai. I also held research positions in
University
of Tubingen,
TIFR - Mumbai,
LIAFA - Paris,
CMI - Chennai, and
University of Warsaw - Poland.
ACM India Honourable Mention 2014 for my PhD
thesis
Regular quantifiers in Logic
Introduction:
Finite automata models complex systems, from computational processes to biological
phenomena. Deterministic one-counter automata (DOCA) extend finite automata with an
integer counter, enabling the modeling of certain infinite-state systems. DOCAs are
strictly more expressive than finite automata, making them promising candidates for replacing finite
automata in applications, provided scalable algorithms can be developed. This research aims to
advance the understanding and applicability of DOCAs.
Contributions: We addressed two key problems.
Equivalence of weighted DOCA: For a large subclass we showed the problem is in P
[fsttcs23, icla25].
To prove this, we introduced a reachability problem. Using combinatorial techniques
along with linear algebra we showed that the problem is in P.
The equivalence problem for the full class remains a fundamental open problem.
Active learning algorithms for DOCAs:
Developed a SAT-based algorithm [tacas25]
that learns a minimal DOCA. Since minimization is NP-hard, we cannot avoid SAT to
learn a minimal DOCA.
Introduction: This work is at the meeting point of two important branches of language theory:
(1) Extension of finite word language theories: This branch explores structures beyond finite words,
such as infinite words and infinite trees.
(2) Characterization of logics: This branch focuses on identifying and classifying logics. The
classic work of Schutzenberger on the equivalence
of first-order logic and aperiodic monoids in finite words falls here.
We study countable words, the largest extension that is known to have a theory of recognizability.
Contributions: In [icalp15] we provided the
first algebraic characterization of intermediate logics like first-order logic (FO), and its various extensions
like FO with cuts, weak MSO, FO with ordinal quantifiers, and FO with scattered quantifiers. The paper
gives a structure theorem for o-monoids. This enables a deep understanding of various classes of o-monoids.
In a subsequent paper, [mfcs16] we showed a similar characterization for FO2.
Subsequently, in a series of papers we characterized various FO extensions like FO[infinity], temporal logic and
provide the first decomposition results for o-monoids [lics19,
fct21, jcss23,
block-product].
Introduction:
Logic provides a precise framework to express mathematical properties unambiguously. It plays a
vital role in areas like descriptive complexity, and set theory
(see survey).
Contributions:
Our work introduced modulo counting operators, thereby enhancing the expressiveness of logics.
Key contributions (see my thesis ) include
(1) Extending Linear temporal logic (LTL) with modulo counting operators, enhancing its expressive-
ness while retaining PSPACE complexity for model checking [m4m11,
atva10].
(2) Extending first-order logic with modulo counting operators [dlt17].
When the logic has the predicate addition, they form highly uniform circuit classes. In
[lics12] we show separation results among these logics.
Geospatial image analysis for Water research (click for details)
Introduction: Remote sensing for water research works on the principle that there is huge difference
between the dielectric constant of water (approximately 80) and dry soil
(approximately 6).
Contributions: We analyse satellite images and in-situ measurements to
estimate properties of rivers like river discharge [esd20].
We are currently working on a method for soil-moisture estimation.
Formal methods in machine learning (click for details)
Pooled testing (with Somenath Biswas) pdf
Epidemiology SIR model (with Somenath Biswas) pdf
Parity games pdf
Logic for computer science pdf
Linear programming: Introduction pdf,
Ellipsoid method pdf
Machine learning, theory: VC dimension pdf
MaxCut approximation pdf
Learning real-time one-counter automata using polynomially many queries,
with Prince Mathew, and Vincent Penelle,
TACAS 2025
(
arXiv,
abstract)
Abstract :
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.
Equivalence of deterministic weighted real-time one-counter automata,
with Prince Mathew, Vincent Penelle, and Prakash Saivasan,
ICLA 2025 (
arXiv ,
abstract)
Abstract :
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.
Algebraic characterizations and block product decompositions for first order logic and
its infinitary quantifier extensions over countable words,
with Bharat Adsul and Saptarshi Sarkar,
JCSS 2023 (
pdf,
abstract)
Abstract :
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
Weighted One-Deterministic-Counter Automata,
with Prince Mathew, Vincent Penelle, and Prakash Saivasan,
FSTTCS 2023 (
arXiv,
abstract)
Abstract :
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.
First-Order logic and its Infinitary Quantifier Extensions over Countable Words,
with Bharat Adsul and Saptarshi Sarkar,
FCT 2021
(
pdf,
full,
abstract)
Abstract :
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.
Coupling threshold theory and satellite image derived channel width to
estimate the formative discharge of Himalayan Foreland rivers
, with K. Gaurav , F. Métivier , R. Sinha , A. Kumar , and S. K. Tandon,
Earth Science Dynamics 2021
(
pdf,
abstract)
Abstract :
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.
Undecidability of MSO+“ultimately periodic”, with
Mikołaj Bojańczyk, Laure Daviaud, Bruno Guillon, and Vincent Penelle,
LMCS 2020
(
pdf,
abstract)
Abstract :
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
U1(X) which says that the distance between consecutive positions in a set X ⊆ N is unbounded. This is
achieved by showing that adding U1 to mso gives a logic with the same expressive power as MSO+U, a
logic on omega-words with undecidable satisfiability.
Block Product for finite monoids with generalized associativity, with
Saptarshi Sarkar, and Bharat Adsul
(
pdf,
abstract)
Abstract :
We give the definition of Block Product
for finite moniods with generalized associativity.
Block products for algebras over countable words and applications to logic, with
Saptarshi Sarkar, and Bharat Adsul,
LICS
2019.
(
pdf,
abstract)
Abstract :
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 char- acterizations of first-order logic (resp. first-order logic with two
variables) in terms of strongly (resp. weakly) iterated block products. We use this to arrive at a complete
analogue of Schu ̈tzenberger-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.
Two-variable first order logic with counting quantifiers: Complexity Results,
with
Kamal Lodaya,
DLT 2017.
(
pdf,
abstract)
Abstract :
Etessami,
Vardi and Wilke showed that satisfiability of two-variable first order
logic FO2[<] on word models is Nexptime-complete.
We extend this upper bound to the slightly stronger logic
FO2[<,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
FOMOD2[<,successor]), satisfiability becomes
Expspace-complete. A
more general counting quantifier, FOCOUNT2[<,successor],
makes the logic undecidable.
Two-variable logic over countable linear orderings, with
Amaldev
Manuel,
MFCS 2016.
(
pdf,
full,
abstract)
Abstract :
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.
Limited Set quantifiers over Countable Linear Orderings, with
Thomas
Colcombet,
ICALP 2015.
(
pdf,
full,
abstract)
Abstract :
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.
Counting quantifiers and linear arithmetic on word models, with
Kamal
Lodaya,
Asian
Logic Conference (ALC), 2014.
(
pdf)
On lower bounds for multiplicative circuits and linear circuits in noncommutative domains, with
V. Arvind and
S. Raja,
CSR, 2014.
(
pdf,
abstract)
Abstract :
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.
Non-definability of
Languages by Generalized First-order Formulas
over (N, +), with
Andreas
Krebs,
LICS 2012.
(
pdf,
full,
abstract)
Abstract :
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 CC0 from FO[<,+]-uniform ACC0.
Expressive Completeness
for
LTL With Modulo Counting and Group
Quantifiers,
Electronic
Notes in Theoretical Comp Sci
(ENTCS),
2011.
(
pdf,
abstract)
Abstract :
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,Th\'erien) is
expressively complete for first order logic with modulo counting
(introduced by Straubing, Th\'erien, Thomas) and
group quantifiers (introduced by Barrington, Immerman,
Straubing).
LTL can be more succinct,
with
Kamal Lodaya,
ATVA 2010 .
(
pdf,
abstract)
Abstract :
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 Th\'erien, 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 Sigmathree-complete.
Ph.D. students
Masters students
Ankita Chand, Divya Mishra, Anshul Moon, Vaishak D. A, Vaibhav (co-guide:Somenath Biswas),
Rashika (co-guide: Sudakshina), Sumitra (co-guide: Sudakshina), Umang Srivatsav
CS510: Foundations of theoretical computer science, Aug-Dec 2024, MTech core.
CS311: Compilers (shared), Jan-May 2024, BTech core.
CS528: Formal methods in machine learning (shared), Jan-May 2024, BTech/MTech elective.
CS510: Foundations of theoretical computer science, Aug-Dec 2023, MTech core.
CS220: Data structures and algorithms, Aug-Dec 2022, BTech core.
CS525: Randomized algorithms, Jan-May 2022, BTech/MTech elective.
CS524: Advanced data structures and algorithms with C++, Aug-Dec 2021, MTech course.
CS220:
Data structures and algorithms , Aug-Dec 2021
video lectures-C/C++
Programming
CS531:
High dimensional data science , Jan-May 2021
video lectures
CS220:
Data structures and algorithms , Aug-Dec 2020
video lectures-C/C++
Programming,
video
lectures-Data Structures and algorithms
CS500: Algorithm design lab, Aug-Dec 2020
CS520:
Combinatorial optimization , Jan-May 2020
CS113:
Data structures and algorithms , July-Dec 2020
CS228:
Logic for computer science , July-Dec 2019
CS570: Verification, July-Dec 2019
CS315:
Advanced algorithms , Jan-May 2019
CS713: Topics in logic and automata theory, July-Dec 2018
CS228:
Logic for computer science , July-Dec 2018
CS101:
Computer programming
, Summer 2018
CS348:
Computer Networks Course , Jan-May 2018
CS 378:
Computer Networks Lab Jan-May 2018
Reading Logic with Prince
Visiting faculty: University of Bordeaux in 2024 (four months)
SERB Matrics grant: Probabilistic pushdown automata
CEFIPRA: Formal verification of adaptive control algorithms
Ministry of Earth Science (completed): River parameter estimation using satellite images
Department research talks: link
Shannon on Creative thinking
Computer science bibliography collections
Computer science conference timelines
Erdos Number
♚
Live chess tournaments
