Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Deterministic Weighted Automata under Partial Observability

Jakub Michaliszyn, Jan Otop

TL;DR

This paper introduces partially-observable deterministic weighted automata (PODWA), where outputs are interval observations rather than exact values, to address learning and synthesis of quantitative specifications under partial information. It analyzes core learning-related problems: equivalence, sample fitting, and minimization, revealing coNP-hardness of equivalence in general but polynomial-time solvability for unary weights, and NP-hardness of minimization—even with unary weights—through careful reductions (e.g., subset sum and $k$-coloring). The results indicate significant obstacles to polynomial-time active learning of PODWA, while suggesting that restricting equivalence notions or focusing on unary-weight fragments could enable feasible learning pipelines. The findings guide future work on robust equivalence notions and restricted PODWA subclasses for practical active learning in quantitative verification contexts.

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

Deterministic Weighted Automata under Partial Observability

TL;DR

This paper introduces partially-observable deterministic weighted automata (PODWA), where outputs are interval observations rather than exact values, to address learning and synthesis of quantitative specifications under partial information. It analyzes core learning-related problems: equivalence, sample fitting, and minimization, revealing coNP-hardness of equivalence in general but polynomial-time solvability for unary weights, and NP-hardness of minimization—even with unary weights—through careful reductions (e.g., subset sum and -coloring). The results indicate significant obstacles to polynomial-time active learning of PODWA, while suggesting that restricting equivalence notions or focusing on unary-weight fragments could enable feasible learning pipelines. The findings guide future work on robust equivalence notions and restricted PODWA subclasses for practical active learning in quantitative verification contexts.

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
Paper Structure (14 sections, 6 theorems, 7 equations, 2 figures)

This paper contains 14 sections, 6 theorems, 7 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Our framework
  3. Results
  4. Related work
  5. Preliminaries
  6. Our framework
  7. Sample fitting
  8. Towards active learning PODWA
  9. Equivalence
  10. Unary weights
  11. Minimization
  12. Minimization by merging.
  13. Conclusions
  14. Appendix

Key Result

lemma 1

$\mathcal{L}_\cup$ is not PODWA-recognizable.

Figures (2)

  • Figure 1: a) The automaton ${\Lambda}_n$. The omitted edges lead to $s$ with weight $0$. b) A minimal automaton equivalent to ${\Lambda}_n$.
  • Figure 2: Two binary PODWA that are equivalent and minimal but not isomorphic.

Theorems & Definitions (14)

  • remark 1
  • lemma 1
  • proof
  • lemma 2
  • proof
  • theorem 1
  • proof
  • theorem 2
  • proof
  • remark 2: The right congruence for DWA
  • ...and 4 more