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 [7]. 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 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.

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 prove the undecidability of MSO on $\omega$-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 $\omega$-words with undecidable satisfiability. As a corollary, 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 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 (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 Schiitzenberger-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.

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.

Etessami et al. [5] showed that satisfiability of two-variable first order logic FO^2 [<] on word models is Nexptime-complete. We extend this upper bound to the slightly stronger logic FO^2 [ <,succ ,≡ ], 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, Thérien et al. [22] (we call this two-variable fragment FOmod ^2 [ <,succ ]), satisfiability becomes Expspace-complete. A more general counting quantifier, FOunC ^2 [ <,succ ], 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 such as 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 over words. We show that all languages with a neutral letter, definable using the addition predicate are also definable with the order predicate as the only numerical predicate. Let S be a subset of monoids. Let L be the logic closed under quantification over the monoids in S. Then we prove that L[<;,+] and L[<;] define the same neutral letter languages. Our result can be interpreted as the Crane Beach conjecture to hold for the logic L[<;,+]. As a consequence 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 as a numerical predicate is necessary for Barrington's theorem to hold and also to simulate majority quantifiers. All these results can be viewed as separation results for highly uniform circuit classes. For example we separate FO[<;,+]-uniform CC0 from FO[<;,+]-uniform ACC0.

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, Therien) is expressively complete for first order logic with modulo counting (introduced by Straubing, Therien, Thomas) and group quantifiers (introduced by Barrington, Immerman, 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 Thérien, 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 and for threshold counting) 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^P_3\)-complete.