Learning and Equivalence of One-Counter Systems
Prince Mathew
Abstract
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.