First-Order logic and its Infinitary Quantifier Extensions over Countable Words
with Bharat Adsul and Saptarshi Sarkar,
Coupling threshold theory and satellite image derived channel width to
estimate the formative discharge of Himalayan Foreland rivers.
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.
with K. Gaurav , F. Métivier , R. Sinha , A. Kumar , and S. K. Tandon,
Earth Science Dynamics 2021
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.
with Somenath Biswas
Notes on Parity games
We look at one-time pooled testing and multiple pooled testing.
Undecidability of MSO+“ultimately periodic”
The notes were made during a lecture series on Parity games. We used notes from Mikołaj Bojańczyk's
page for the lecture series.
Mikołaj Bojańczyk, Laure Daviaud, Bruno Guillon, and Vincent Penelle, LMCS 2020
Block Product for finite monoids with generalized associativity
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.
Saptarshi Sarkar, and Bharat Adsul
Block products for algebras over countable words and applications to logic
We give the definition of Block Product for finite moniods with generalized associativity.
Saptarshi Sarkar, and Bharat Adsul, LICS 2019
Lecture notes: Logic for computer scientists
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
Lecture notes prepared for the Logic course (CS228)
with Kamal Lodaya
Two-variable logic over
countable linear orderings
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
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
more general counting quantifier, FOCOUNT2[<,successor],
makes the logic undecidable.
, with Amaldev
, MFCS 2016
Limited Set quantifiers
Countable Linear Orderings
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
, ICALP 2015
linear arithmetic on word models
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.
, with Kamal Lodaya
Logic Conference (ALC), 2014
On lower bounds for
multiplicative circuits and linear circuits in
, with V.
and S. Raja,
Languages by Generalized First-order Formulas
over (N, +)
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
entries come from noncommutative rings. We show some lower
bounds in this setting as well.
, with Andreas
, LICS 2012
LTL With Modulo Counting and Group
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.
Notes in Theoretical Comp Sci
LTL can be more succinct
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,
with Kamal Lodaya
, ATVA 2010.
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.