Jan Otop

ECAI Conference 2025 Conference Paper

Active Automata Learning with Advice

• Michal Fica
• Jan Otop

We present an extended automata learning framework that combines active automata learning with deductive inference. The learning algorithm asks membership and equivalence queries as in the original framework, but it is also given advice, which is used to infer answers to queries when possible and reduce the burden on the teacher. We consider advice given via string rewriting systems, which specify equivalence of words w. r. t. the target languages. The main motivation for the proposed framework is to reduce the number of queries. We show how to adapt Angluin-style learning algorithms to this framework with low overhead. Finally, we present empirical evaluation of our approach and observe substantial improvement in query complexity.

MFCS Conference 2025 Conference Paper

Minimization of Deterministic Finite Automata Modulo the Edit Distance

• Jakub Michaliszyn
• Jan Otop

We propose a novel approach to minimization of deterministic finite automata (DFA), in which the DFA is further minimized at the expense of relaxing equality of languages to merely a similarity. As the notion of similarity of languages, we consider the edit distance between languages ℒ, ℒ', i. e. , the minimal number of edits necessary to transform any word from ℒ to some word from ℒ' and vice versa. In this paper we address two problems: minimization up to a predetermined edit distance given in the input, and minimization up to a bounded edit distance, in which there has to be an upper bound on the number of edits, but it is not specified. We show the first problem to be PSpace {}-complete and that the second problem is in Σ₂^p, and both NP-hard and coNP-hard. We show that if we limit how many strongly connected components can be visited by a single run (i. e. , bounded SCC-depth), the problem becomes NP-complete. We also establish maximal subclasses of DFA over which minimization up to a bounded edit distance can be performed in polynomial time. Additionally, we provide a succinct overview of alternative metrics for assessing language similarity.

JELIA Conference 2023 Conference Paper

Deterministic Weighted Automata Under Partial Observability

• Jakub Michaliszyn
• Jan Otop

Abstract Weighted automata is a basic tool for specification in quantitative verification, which allows to express quantitative features of analysed systems such as resource consumption. Quantitative specification can be assisted by automata learning as there are classic results on Angluin-style learning of weighted automata. The existing work assumes perfect information about the values returned by the target weighted automaton. In assisted synthesis of a quantitative specification, knowledge of the exact values is a strong assumption and may be infeasible. In our work, we address this issue by introducing a new framework of partially-observable deterministic weighted automata, in which weighted automata return intervals containing the computed values of words instead of the exact values. We study the basic properties of this framework with the particular focus on the challenges of active learning partially-observable deterministic weighted automata.

MFCS Conference 2022 Conference Paper

Learning Deterministic Visibly Pushdown Automata Under Accessible Stack

• Jakub Michaliszyn
• Jan Otop

We study the problem of active learning deterministic visibly pushdown automata. We show that in the classical L^*-setting, efficient active learning algorithms are not possible. To overcome this difficulty, we propose the accessible stack setting, where the algorithm has the read and write access to the stack. In this setting, we show that active learning can be done in polynomial time in the size of the target automaton and the counterexamples provided by the teacher. As counterexamples of exponential size are inevitable, we consider an algorithm working with words in a compressed representation via (visibly) Straight-Line Programs. Employing compression allows us to obtain an algorithm where the teacher and the learner work in time polynomial in the size of the target automaton alone.

AIJ Journal 2022 Journal Article

Learning infinite-word automata with loop-index queries

• Jakub Michaliszyn
• Jan Otop

Highlights Conference 2021 Conference Abstract

Active Learning Infinite-Word Automata

• Jan Otop

Regular languages can be actively learned with membership and equivalence queries in polynomial time. The learning algorithm, called the L^* algorithm, constructs iteratively the right congruence relation of a given regular language L, and returns the minimal DFA recognizing L. The L^* algorithm has been adapted to various types of automata: tree automata, weighted automata, nominal automata. However, an extension to infinite-word automata has been elusive. I will discuss why extending L^* to infinite-word automata is difficlut. Next, I will present an alternative approach, in which we learn the automaton rather than its language. That is, we consider a hidden target automaton T and the learning algorithm asks queries about the language of T and its structure. The learning algorithm returns an automaton equivalent to T and structurally similar to T. We consider T to be either a Deterministic Buechi Automaton or a LimAvg-automaton.

IJCAI Conference 2021 Conference Paper

Minimization of Limit-Average Automata

• Jakub Michaliszyn
• Jan Otop

LimAvg-automata are weighted automata over infinite words that aggregate weights along runs with the limit-average value function. In this paper, we study the minimization problem for (deterministic) LimAvg-automata. Our main contribution is an equivalence relation on words characterizing LimAvg-automata, i. e. , the equivalence classes of this relation correspond to states of an equivalent LimAvg-automaton. In contrast to relations characterizing DFA, our relation depends not only on the function defined by the target automaton, but also on its structure. We show two applications of this relation. First, we present a minimization algorithm for LimAvg-automata, which returns a minimal LimAvg-automaton among those equivalent and structurally similar to the input one. Second, we present an extension of Angluin's L^*-algorithm with syntactic queries, which learns in polynomial time a LimAvg-automaton equivalent to the target one.

ECAI Conference 2020 Conference Paper

Learning Deterministic Automata on Infinite Words

• Jakub Michaliszyn
• Jan Otop

We study active learning of deterministic infinite-words automata. In our framework, the teacher answers not only membership and equivalence queries, but also provides the loop index of the target automaton on wv ω, which is the minimal number of letters of wv ω past which the target automaton reaches the final cycle on wv ω. We argue that in potential applications if one can answer Boolean part in membership (and equivalence) queries, one can compute the loop index as well. Our framework is similar to the one of Angluin’s L * -algorithm, but the crucial difference is that the queries about the loop index depend on a particular automaton representing an ω-regular language. This allows us to bypass the NP-hardness coming from the minimisation problem for deterministic BÂĺuchi automata and provide a polynomial-time algorithm for learning deterministic Büchi automata. We adapt this algorithm to deterministic infinite-word weighted automata with LIMINF and LIMSUP value functions, which, treated as parity automata, can recognize all ω-regular languages.

MFCS Conference 2016 Conference Paper

Nested Weighted Limit-Average Automata of Bounded Width

• Krishnendu Chatterjee
• Thomas A. Henzinger
• Jan Otop

While weighted automata provide a natural framework to express quantitative properties, many basic properties like average response time cannot be expressed with weighted automata. Nested weighted automata extend weighted automata and consist of a master automaton and a set of slave automata that are invoked by the master automaton. Nested weighted automata are strictly more expressive than weighted automata (e. g. , average response time can be expressed with nested weighted automata), but the basic decision questions have higher complexity (e. g. , for deterministic automata, the emptiness question for nested weighted automata is PSPACE-hard, whereas the corresponding complexity for weighted automata is PTIME). We consider a natural subclass of nested weighted automata where at any point at most a bounded number k of slave automata can be active. We focus on automata whose master value function is the limit average. We show that these nested weighted automata with bounded width are strictly more expressive than weighted automata (e. g. , average response time with no overlapping requests can be expressed with bound k=1, but not with non-nested weighted automata). We show that the complexity of the basic decision problems (i. e. , emptiness and universality) for the subclass with k constant matches the complexity for weighted automata. Moreover, when k is part of the input given in unary we establish PSPACE-completeness.

IJCAI Conference 2016 Conference Paper

Querying Data Graphs with Arithmetical Regular Expressions

• Maciej Graboń
• Jakub Michaliszyn
• Jan Otop
• Piotr Wieczorek

We propose a query language LARE for graphs whose edges are labelled by a finite alphabet and nodes store unbounded data values. LARE is based on a variant of regular expressions with memory. Queries of LARE can compare quantities of memorised graph nodes and their neighbourhoods. These features allow us to express a number of natural properties, while keeping the data complexity (with a query fixed) in non-deterministic logarithmic space. We establish an algorithm that works efficiently not only with LARE, but also with a wider language defined using effective relational conditions, another formalism we propose.

Highlights Conference 2013 Conference Abstract

Elementary modal logics -- decidability and complexity

• Jakub Michaliszyn
• Jan Otop
• Emanuel Kieronski

Modal logic is called "elementary" if it is considered over class of frames definable by a first-order formula. Different formulae lead to different logics, and many of them find their applications in computer science. The aim of the Highlights conference talk is to present a wide picture of the latest research on the satisfiability problem of elementary modal logics. The talk will provide all the necessarily definitions, discuss the motivation, summarise the recent research papers on this topic, and discuss some open problems.

CSL Conference 2013 Conference Paper

Elementary Modal Logics over Transitive Structures

• Jakub Michaliszyn
• Jan Otop

We show that modal logic over universally first-order definable classes of transitive frames is decidable. More precisely, let K be an arbitrary class of transitive Kripke frames definable by a universal first-order sentence. We show that the global and finite global satisfiability problems of modal logic over K are decidable in NP, regardless of choice of K. We also show that the local satisfiability and the finite local satisfiability problems of modal logic over K are decidable in NExpTime.

GandALF Workshop 2012 Workshop Paper

Satisfiability vs. Finite Satisfiability in Elementary Modal Logics

• Jakub Michaliszyn
• Jan Otop
• Piotr Witkowski

We study elementary modal logics, i. e. modal logic considered over first-order definable classes of frames. The classical semantics of modal logic allows infinite structures, but often practical applications require to restrict our attention to finite structures. Many decidability and undecidability results for the elementary modal logics were proved separately for general satisfiability and for finite satisfiability [11, 12, 16, 17]. In this paper, we show that there is a reason why we must deal with both kinds of satisfiability separately – we prove that there is a universal first-order formula that defines an elementary modal logic with decidable (global) satisfiability problem, but undecidable finite satisfiability problem, and, the other way round, that there is a universal formula that defines an elementary modal logic with decidable finite satisfiability problem, but undecidable general satisfiability problem.

LPAR Conference 2004 Conference Paper

On a Semantic Subsumption Test

• Jerzy Marcinkowski
• Jan Otop
• Grzegorz Stelmaszek

Abstract We observe, that subsumption of clauses (in the language of first order logic), so far understood as a syntactic notion, can also be defined by semantical means. Subsumption is NP-complete and testing subsumption takes roughly half of the running time of a typical first order resolution-based theorem prover. We also give some experimental evidence, that replacing syntactic indexing for subsumption by our semantic Monte Carlo technique can, in some situations, significantly decrease the cost of subsumption testing. Finally, we provide some evidence that a similar semantic idea can be probably successfully used for testing for AC matching, which is another NP-complete problem whose millions of instances are being solved by theorem provers.