Prince Mathew

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 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 time exponential in the size of the DOCA under learning. Furthermore, previous learning algorithms are ''grey-box'' algorithms relying on an additional query type - counter value queries - where the teacher must return the counter value for a given word. Our algorithm is a ''black-box'' algorithm, that runs in polynomial time and can learn DOCAs without any restriction. 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 automaton 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 thesis contributes to the study of active learning and equivalence of one-counter systems. The first part of this thesis focuses on developing a new approach for active learning of deterministic real-time one-counter automata (DROCA). Traditional approaches to learning DROCA often involve learning an initial portion of an infinite behavioural graph. The aim is to identify a repetitive structure in the graph that defines the overall behaviour of the DROCA. However, this repetitive structure often requires constructing an exponentially large graph, leading to an exponential runtime and number of queries. In contrast, our SAT-based method reduces the number of queries to a polynomial number, significantly improving the efficiency of learning algorithms for DROCA. Furthermore, it learns a minimal counter-synchronous DROCA recognising the language making it more feasible for practical applications. We also introduce improved equivalence checking algorithms for counter-synchronised one-counter automata that is used in our learning algorithm. This helps to obtain much smaller counter-examples on equivalence queries. Additionally, we present an even faster equivalence check for the special case of visibly one-counter automata.

The second part of the thesis introduces real-time one-deterministic-counter automata (RODCA). These are real-time one-counter automata 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. We prove that the equivalence of WRODCA over fields is in P. This is a step towards resolving the open question of the equivalence problem of weighted one-counter automata. We also considered boolean RODCA and showed that the equivalence problem for (nondeterministic) boolean RODCA is in PSPACE. In contrast, it is undecidable for (nondeterministic) boolean one-counter automata. Additionally, a faster equivalence-checking method is proposed for the special case of deterministic weighted real-time one-counter automata. The thesis also explores the regularity and covering problems for WRODCA, and shows that they are in P.

Keywords: One-counter automata, Equivalence, Active Learning, Weighted automata, Reachability, SAT solver, Regularity, Covering.

In this paper, we are interested in weighted one-counter automata whose transitions are assigned a weight from a fixed field. In particular, we consider deterministic weighted real-time one-counter automaton (DWROCA). A DWROCA is a deterministic real-time one-counter automaton whose transitions are assigned a weight. 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 for checking the equivalence of two DWROCAs. This gives a better polynomial-time algorithm for checking the equivalence of DWROCAs.

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 𝖯. These reachability problems help us to show that the equivalence problem of weighted odcas over fields is in 𝖯 by adapting the equivalence proof of deterministic real-time ocas [Stanislav Böhm and Stefan Göller, 2011] by Böhm et al. This is a step towards resolving the open question of the equivalence problem of weighted ocas. Finally, 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 𝖯. 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.

This paper proposes an efficient classifier based on continuous cellular automata with promising running time and classification accuracy. The classifier model is capable of processing data sets containing large number of numeric as well as non-numeric attributes. It performs effective pre-processing of numeric and nominal attributes to identify the most relevant ones. It also prunes out unnecessary computations by limiting stabilisation of the cellular automata during the training phase. The classifier also employs various techniques to reduce the number of incorrect classifications and overfitting of data. A number of experiments were conducted to evaluate the performance of the proposed classifier by changing various parameters during the training phase. Evaluations show that the classifier out-performs existing rule-based classifiers in terms of accuracy.

The ability to understand music score is a basic requirement for learning music. This paper proposes a mathematical method to find the pitch of a musical note from digital image of sheet music and a classification-based method for detecting the duration of a music note. In a sheet music, the horizontal direction can be associated with the notes starting time, whilst the vertical direction can be associated with pitch. The symbols used for a note represents its duration. Music scores sometimes need to be transposed or slightly modified, having the score in a digital format greatly reduces the time and effort required to do these. In this paper, we make use of techniques such as Run Length Encoding (RLE), Horizontal projection and Vertical Projection (X & Y projections) for Segmentation and attribute extraction. For note recognition, a classifier based system is used which returns the duration of the given input symbol. The pitch, duration and position of notes are finally given as input to a midi generation module, which generates a MIDI file corresponding to the given input music notation. There are several other applications to Optical Music Recognition (OMR) systems. Converting music scores in Braille code for the blind is yet another application of an OMR system.

Active automata learning is a key technique in formal methods, particularly for model inference and verification. In the classical setting introduced by Angluin’s L* algorithm, a learner interacts with a teacher through membership and equivalence queries to infer a minimal deterministic finite automaton (DFA) for an unknown regular language L. Membership queries check word inclusion in L, while equivalence queries verify whether a proposed hypothesis DFA matches L, returning a counterexample if not. This approach runs in time polynomial in the minimal DFA size and the longest counterexample. We extend this framework to deterministic one-counter automata (DOCA). DOCA are finite-state machines equipped with a non-negative integer counter that can be incremented, decremented, or reset. The presence of the counter allows DOCA to recognise certain non-regular, context-free languages such as {a^n b^n | n > 0}, making them a natural candidate for modelling some infinite state systems that arise in formal verification. We present OL*, a polynomial-time active learning algorithm for DOCA. Unlike previous exponential-time syntactic approaches for learning one-counter automata, OL* is semantic—it learns the language of the target automaton without any knowledge of the DOCA structure. However, unlike L*, where the teacher can return any counter-example, we assume that the teacher always provides a minimal counter-example in response to an equivalence query. OL* can also be used to approximate DOCA minimisation, a problem whose exact version is NP-hard even for certain subclasses of DOCA. Future work includes improving the efficiency of equivalence checking and exploring richer query types to enhance practical applicability.

In this talk, 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 automaton 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.

In this talk, 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 automaton 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 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.

In this presentation, we introduce a novel method for active learning of a minimal-sized visibly one-counter automaton (VOCA) using SAT solver. We follow Angluin's L* algorithm. The algorithm uses only a polynomial number of membership or equivalence queries. All the existing literature, including the algorithm presented by Neider and Löding for learning VOCA, requires exponentially many queries relative to the size of a minimal VOCA recognising the given language. Our approach eliminates the necessity to observe the VOCAs behaviour up to exponentially large counter values. This sets it apart from existing techniques that rely on identifying repetitive patterns in behaviour graphs of exponential size. Michaliszyn and Otop observed that the problem of finding the minimal VOCA is NP-Complete. If a polynomial time algorithm for learning the minimal VOCA exists, it could be employed to minimise VOCA in polynomial time. Consequently, a learning algorithm for VOCA that achieves minimal representation in polynomial time does not exist. In the latter part of the work, we looked at learning Deterministic real-time one-counter automata (DROCA). However, we make use of an additional query, called counter-value query - the student gives the teacher a word, and the teacher returns the counter-value reached on traversing the word in the DROCA. We show that learning DROCA can done using polynomially many queries within this framework. This improves the existing result by Bruyère et al. that needed an exponential number of queries, space and time for learning DROCA.

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 𝖯. These reachability problems help us to show that the equivalence problem of weighted odcas over fields is in 𝖯 by adapting the equivalence proof of deterministic real-time ocas [Stanislav Böhm and Stefan Göller, 2011] by Böhm et al. This is a step towards resolving the open question of the equivalence problem of weighted ocas. Finally, 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 𝖯. 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 introduce One-deterministic-counter automata (ODCA), one-counter automata where all runs labeled by a given word exhibit the same counter effect. The talk will specifically focus on weighted ODCAs. We present a novel problem known as the co-VS (complement to a vector space) reachability problem. By leveraging properties of matrices and vector spaces, a pseudo-pumping lemma is established, proving that the Co-VS reachability problem is in P. Furthermore, we demonstrate that the lexicographically minimal witness for this problem has a special form. Consequently, it follows that the equivalence problem of ODCAs is also in P. This is joint work with Dr. Sreejith A.V., Dr. Vincent Penelle, and Dr. Prakash Saivasan.

We introduce one deterministic-counter automata (ODCA), which are one-counter automata where all runs labelled by a given word have the same counter effect, a property we call counter-determinacy. ODCAs are an extension of visibly one-counter automata - one-counter automata (OCA), where the input alphabet determines the actions on the counter. They are a natural way to introduce non-determinism/weights to OCAs while maintaining the decidability of crucial problems that are undecidable on general OCAs. For example, the equivalence problem is decidable for deterministic OCAs, whereas it is undecidable for non-deterministic OCAs. We consider both non-deterministic and weighted ODCAs. Our work shows that the equivalence problem is decidable in polynomial time for weighted ODCAs over a field and polynomial space for non-deterministic ODCAs. As a corollary, we get that the regularity problem, i.e., the problem of checking whether an input weighted ODCA is equivalent to some weighted automaton, is also in polynomial time. Furthermore, we show that the covering and coverable equivalence problems for uninitialised weighted ODCAs are decidable in polynomial time. We also introduce a few reachability problems that are of independent interest and show that they are in P. These reachability problems later help in solving the equivalence problem.