pith. machine review for the scientific record. sign in

arxiv: 2604.17370 · v1 · submitted 2026-04-19 · 💻 cs.FL

Recognition: unknown

Weighted Automata and Regular Expressions for Financial Systems

Manfred Droste , Vitaly N\"urnberg
Authors on Pith no claims yet

Pith reviewed 2026-05-10 05:37 UTC · model grok-4.3

classification 💻 cs.FL
keywords weighted automataregular expressionsfinancial modelingKleene-Schützenberger theoremquantitative analysisdecision problemspayoff computation
0
0 comments X

The pith

Weighted finite finance automata correspond to weighted finance regular expressions via a Kleene-Schützenberger theorem, enabling formal analysis of quantitative financial properties.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces weighted finite finance automata as a way to represent financial systems whose behavior depends on uncertain variables such as prices and rates. It defines weighted finance regular expressions as a declarative notation for the same systems. A correspondence theorem links the two formalisms and supplies algorithms that convert one representation into the other. The resulting framework supports compositional description of instruments and strategies together with algorithms for computing extremal payoffs and identifying tractable subclasses.

Core claim

The paper establishes a Kleene-Schützenberger-type correspondence between weighted finite finance automata and weighted finance regular expressions, together with effective translation procedures between the two formalisms. This correspondence supplies a compositional language-theoretic model for quantitative financial properties driven by uncertain economic variables and permits algorithmic solution of decision and optimization problems such as extremal-payoff computation on expressive yet tractable subclasses.

What carries the argument

The Kleene-Schützenberger correspondence between weighted finite finance automata (WFFAs) and weighted finance regular expressions, which supplies bidirectional translations and supports evaluation of payoffs across market scenarios.

If this is right

  • Financial instruments and trading strategies can be evaluated compositionally across multiple market scenarios.
  • Extremal payoffs can be computed algorithmically for given automata or expressions.
  • Expressive yet computationally tractable subclasses admit efficient decision procedures for optimization problems.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same automata could serve as the backend for scenario generators that produce payoff distributions for risk calculations.
  • Translations between automata and expressions might allow automatic verification of regulatory constraints expressed as regular properties.

Load-bearing premise

Financial systems driven by uncertain economic variables can be faithfully represented as weighted automata whose weights capture quantitative payoffs without losing essential market dynamics or requiring domain-specific extensions beyond the stated model.

What would settle it

A concrete financial scenario whose payoff sequence cannot be generated by any weighted finite automaton whose weights stay within the model’s finite state space and translation rules.

Figures

Figures reproduced from arXiv: 2604.17370 by Manfred Droste, Vitaly N\"urnberg.

Figure 1
Figure 1. Figure 1: Recall that a monoid (M, ·, 1) consists of a set M, a binary operation · : M × M → M, which is associative (i.e., (a · b) · c = a · (b · c) for all a, b, c ∈ M), and a unit element 1 ∈ M such that m·1 = 1·m = m for all m ∈ M. The monoid M is called commutative if a · b = b · a for all a, b ∈ M. A semiring is a structure S = (S, ⊕, ⊗, 0, 1) where (S, ⊕, 0) is a commutative monoid and (S, ⊗, 1) is a monoid, … view at source ↗
Figure 1
Figure 1. Figure 1: Graphical representation of the finance word from Example 2.1. [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Graphical representations of the WFFAs from Examples 3.3 and 3.6. [PITH_FULL_IMAGE:figures/full_fig_p007_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: WFFAs for the European call option. (a) Long position: payoff obtained via max-aggregation over runs. (b) Short position: guarded transitions enforce case distinction ST > K and ST ≤ K. Example 3.8. We now consider the short-position profit of a European call option (cf. [13, Ch. 14]). Recall that π short eur (ST ) = c0 − max{ST − K, 0}. Equivalently, π short eur (ST ) = c0 + min{K − ST , 0}. Unlike the lo… view at source ↗
Figure 4
Figure 4. Figure 4: WFFAs for (a) an American call option and (b) a buy limit order. [PITH_FULL_IMAGE:figures/full_fig_p009_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: WFFA AF from the proof of Lemma 6.12. 31 [PITH_FULL_IMAGE:figures/full_fig_p031_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: WFFAs AF1 and AF2 from the proof of Theorem 6.10(a). (b) Let F : DΣ ∗ → S be defined by F(⊥d) = d+1 for all d ∈ D and F(w) = 0 for all w ∈ DΣ ∗ with |w| ̸= 1. Clearly, F is proper. Consider the automaton AF ∈ WFFAΣ,F(⟨⟨S⟩⟩F ) depicted in [PITH_FULL_IMAGE:figures/full_fig_p033_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: WFFA AF from the proof of Theorem 6.10(b). Lemma A.11 (Lemma 6.13). Let F be a finance semiring with an additive data-binding function. Then, PF satisfies the bounded sum property and B(PF) ≤ 2. Proof. For any k ∈ N≥1, let π1, . . . , πk ∈ PF and define e = [π1 ⊕ . . . ⊕ πk]. Since ⊕ is commutative, we may assume that π1, . . . , πl ∈ S for some l ≤ k and πl+1, . . . , πk ∈ ⟨⟨S⟩⟩F . Then e = [s1 ⊕ . . . ⊕ … view at source ↗
Figure 8
Figure 8. Figure 8: WFFA AF from the proof of Theorem A.22(b). Now let F ′ = −F. Then for all finance words w = ⊥d1,...,dn ∈ DΣ ∗ , F ′ (⊥d1,d2 ) = ( min{−d1, −d2}, if n = 2, −∞, otherwise. We show that F ′ ∈/ [[WFFAΣ,F]]. Suppose, towards a contradiction, that there exists an automaton A = (Q, I, T, F, wtI , wtT , wtF ) ∈ WFFAΣ,F such that [[A]] = F ′ . By Theorem 6.22, we may assume without loss of generality that A ∈ WFFAΣ… view at source ↗
Figure 9
Figure 9. Figure 9: It is straightforward to verify that [[Aea ]] = [[ea]] and [[Asε ]] = [[sε]]. Thus, the claims (a) and (b) follow. 40 [PITH_FULL_IMAGE:figures/full_fig_p040_9.png] view at source ↗
Figure 9
Figure 9. Figure 9: WFFAs Aea and Asε from the proof of Lemma 7.7. Lemma A.24 (Lemma 7.8). Let E ⊆ EF be an arbitrary collection of F-expressions and R ∈ REGε-free Σ,F (E). Then, there exists A ∈ WFFAτ Σ,F (E) such that [[A]] = [[R]]. Proof. We proceed by induction on the structure of R. • For R = ea with e ∈ E and a ∈ Σ, apply Lemma 7.7(a). • For R = R1 ⊕ R2, apply the induction hypothesis for R1 and R2 and Corollary 6.9(a).… view at source ↗
read the original abstract

We introduce weighted finite finance automata (WFFA), a formal framework for modeling and analyzing quantitative properties of financial systems driven by uncertain economic variables such as stock prices, interest rates, and exchange rates. The model provides a compositional and language-theoretic approach to scenario-based financial analysis, enabling systematic evaluation of financial instruments and trading strategies. To specify such systems, we introduce weighted finance regular expressions, a declarative language for quantitative financial properties. We establish a Kleene-Sch\"utzenberger-type correspondence between WFFAs and weighted finance regular expressions, together with effective translation procedures between the two formalisms. On the algorithmic side, we investigate fundamental decision and optimization problems for WFFAs, including the computation of extremal payoffs, and identify expressive yet computationally tractable subclasses. These results provide a foundation for formal, compositional, and efficient analysis of financial systems under multiple market scenarios.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 3 minor

Summary. The paper introduces weighted finite finance automata (WFFAs) to model quantitative properties of financial systems driven by uncertain variables such as stock prices and interest rates. It defines weighted finance regular expressions as a declarative specification language for these properties. The central result is a Kleene-Schützenberger-type equivalence between WFFAs and the expressions, accompanied by effective translations in both directions. The work further studies decision and optimization problems on WFFAs, including extremal-payoff computation, and identifies expressive yet tractable subclasses.

Significance. If the correspondence and translations hold, the manuscript supplies a compositional, language-theoretic framework for scenario-based financial analysis that directly leverages existing weighted-automata algorithms. The tractable-subclass results are especially useful for practical verification of trading strategies, while the effective translations enable declarative specification without sacrificing algorithmic access. These contributions extend standard semiring-weighted automata theory to a finance setting in a manner that preserves the usual inductive proofs.

major comments (1)
  1. [§3] §3, Theorem 3.1: the inductive proof of the expression-to-automaton direction assumes the underlying semiring is complete for the star operator, yet the paper does not verify that the chosen payoff semiring (with possible negative or unbounded weights) satisfies this; this property is load-bearing for the claimed effective translation.
minor comments (3)
  1. The abstract states that translations are 'effective' but never reports their asymptotic complexity; adding a brief complexity statement after each construction would clarify practicality.
  2. [§2] Notation for the semiring operations (⊕, ⊗) is used in §2 before being formally introduced; a short preliminaries subsection would prevent reader confusion.
  3. [§4] Figure 2 (example WFFA) omits explicit weight labels on two transitions; the accompanying text refers to them but the diagram itself is incomplete.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We appreciate the referee's positive assessment of the manuscript and the recommendation for minor revision. We address the major comment below and will revise the manuscript to incorporate the requested clarification.

read point-by-point responses

  1. Referee: [§3] §3, Theorem 3.1: the inductive proof of the expression-to-automaton direction assumes the underlying semiring is complete for the star operator, yet the paper does not verify that the chosen payoff semiring (with possible negative or unbounded weights) satisfies this; this property is load-bearing for the claimed effective translation.

    Authors: We agree that the completeness of the semiring for the star operator is essential to the inductive proof of Theorem 3.1. The payoff semiring is introduced in Section 2 as the structure (ℝ ∪ {−∞, +∞}, min, +) (or its max-plus dual) to model extremal payoffs. While this semiring is known to be complete in the literature on weighted automata when restricted to bounded weights or finite scenario sets (as assumed throughout our financial models), we did not explicitly verify the condition in the presence of negative or unbounded weights. We will add a short lemma or remark in the revised version confirming that the star operator remains well-defined under our modeling assumptions (finite automata and scenario-bounded payoffs), thereby preserving the effective translation. This is a clarification rather than a change to the results. revision: yes

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper defines weighted finite finance automata (WFFAs) and weighted finance regular expressions as new objects, then states a Kleene-Schützenberger-type correspondence together with effective translations. This is a standard inductive construction once the underlying semiring and semantics are fixed; the abstract gives no indication that the finance-specific weights or payoff computations are used to define the automata or expressions in terms of each other, nor does it rely on self-citation for the core theorem. The decision and optimization results are presented as separate algorithmic investigations rather than as inputs to the correspondence. No load-bearing step reduces by construction to a fitted parameter or prior self-referential claim.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 2 invented entities

The central claim rests on the standard Kleene-Schützenberger theorem being adaptable to the new finance-weighted setting and on the assumption that financial payoffs can be represented as weights in a semiring without additional structure.

axioms (2)
  • standard math Kleene-Schützenberger theorem holds for the chosen weight structure in the finance automata model
    Invoked to establish the equivalence between automata and expressions.
  • domain assumption Financial systems with uncertain variables admit a compositional automata representation
    Required for the model to apply to stock prices, interest rates, and trading strategies.
invented entities (2)
  • Weighted finite finance automata (WFFA) no independent evidence
    purpose: Model quantitative properties of financial systems under uncertainty
    New formalism introduced to capture payoffs driven by economic variables.
  • Weighted finance regular expressions no independent evidence
    purpose: Declarative specification of quantitative financial properties
    New language paired with the automata for specification and translation.

pith-pipeline@v0.9.0 · 5439 in / 1391 out tokens · 32949 ms · 2026-05-10T05:37:21.510876+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

36 extracted references

  1. [1]

    Almagor, U

    S. Almagor, U. Boker, and O. Kupferman,What’s decidable about weighted automata?, Information and Computation282(2022)

    2022

  2. [2]

    Babari, M

    P. Babari, M. Droste, and V. Perevoshchikov,Weighted register automata and weighted logic on data words, Theoretical Computer Science744(2018), 3–21

    2018

  3. [3]

    Babel, P

    K. Babel, P. Daian, M. Kelkar, and A. Juels,Clockwork finance: automated analysis of economic security in smart contracts, IEEE Symposium on Security and Privacy (Los Alamitos, CA), IEEE Computer Society, 2023, pp. 622–639

    2023

  4. [4]

    Bacci, P

    G. Bacci, P. Bouyer, U. Fahrenberg, K. G. Larsen, N. Markey, and P.-A. Reynier, Optimal and robust controller synthesis using energy timed automata with uncertainty, Formal Aspects of Computing33(2021), no. 1, 3–25

    2021

  5. [5]

    Baier and J.-P

    C. Baier and J.-P. Katoen,Principles of model checking, MIT Press, Cambridge, MA, 2008

    2008

  6. [6]

    J. C. Cox, S. A. Ross, and M. Rubinstein,Option pricing: a simplified approach, Journal of Financial Economics7(1979), no. 3, 229–263

    1979

  7. [7]

    Droste, W

    M. Droste, W. Kuich, and H. Vogler (eds.),Handbook of weighted automata, Springer, Berlin, 2009

    2009

  8. [8]

    Droste and D

    M. Droste and D. Kuske,Skew and infinitary formal power series, Theoretical Computer Science366(2006), no. 2, 199–227

    2006

  9. [9]

    Droste and V

    M. Droste and V. Perevoshchikov,Multi-weighted automata and MSO logic, Theory of Computing Systems59(2016), no. 2, 231–261

    2016

  10. [10]

    Droste and G

    M. Droste and G. Rahonis,Weighted automata and weighted logics with discounting, Theoretical Computer Science410(2009), no. 37, 3481–3494

    2009

  11. [11]

    1, European Mathematical Society Publishing House, Z¨ urich, 2021, pp

    Manfred Droste and Dietrich Kuske,Weighted automata, Handbook of Automata Theory (Jean-´Eric Pin, ed.), vol. 1, European Mathematical Society Publishing House, Z¨ urich, 2021, pp. 113–150

    2021

  12. [12]

    Eilenberg,Automata, languages, and machines, vol

    S. Eilenberg,Automata, languages, and machines, vol. b, Academic Press, New York, 1974

    1974

  13. [13]

    F. J. Fabozzi (ed.),Handbook of finance: Valuation, financial modeling, and quantitative tools, Wiley, Hoboken, NJ, 2008

    2008

  14. [14]

    Foucault, M

    T. Foucault, M. Pagano, and A. R¨ oell,Market liquidity, Oxford University Press, Oxford, 2013. 25

    2013

  15. [15]

    Garg and S

    M. Garg and S. Sarswat,The design and regulation of exchanges: a formal approach, FSTTCS 2022 (Wadern), LIPIcs, vol. 250, Schloss Dagstuhl – Leibniz-Zentrum f¨ ur Informatik, 2022, pp. 1–21

    2022

  16. [16]

    Gastin and B

    P. Gastin and B. Monmege,A unifying survey on weighted logics and weighted automata, Soft Computing22(2018), no. 4, 1047–1065

    2018

  17. [17]

    B. K. Hassani,Scenario analysis in risk management: Theory and practice in finance, Springer, Cham, 2016

    2016

  18. [18]

    J. E. Hopcroft and J. D. Ullman,Introduction to automata theory, Addison-Wesley, Reading, MA, 1979

    1979

  19. [19]

    J. C. Hull,Options, futures, and other derivatives, Prentice Hall, Upper Saddle River, NJ, 1993

    1993

  20. [20]

    S. C. Kleene,Representation of events in nerve nets and finite automata, Automata Studies, Princeton University Press, Princeton, NJ, 1956, pp. 3–42

    1956

  21. [21]

    Kruschwitz and A

    L. Kruschwitz and A. Loeffler,Discounted cash flow, John Wiley & Sons, Chichester, 2005

    2005

  22. [22]

    Kuich and A

    W. Kuich and A. Salomaa,Semirings, automata, languages, Springer, Berlin, 1986

    1986

  23. [23]

    K. G. Larsen, G. Behrmann, E. Brinksma, A. Fehnker, T. Hune, P. Pettersson, and J. Romijn,As cheap as possible: efficient cost-optimal reachability for priced timed automata, CAV 2001 (Berlin), LNCS, vol. 2102, Springer, 2001, pp. 493–505

    2001

  24. [24]

    D. G. Luenberger,Investment science, Oxford University Press, Oxford, 1999

    1999

  25. [25]

    Natenberg,Option volatility and pricing, McGraw-Hill, New York, 2014

    S. Natenberg,Option volatility and pricing, McGraw-Hill, New York, 2014

    2014

  26. [26]

    M. O. Rabin,Probabilistic automata, Information and Control6(1963), no. 3, 230–245

    1963

  27. [27]

    M. O. Rabin and D. Scott,Finite automata and their decision problems, IBM Journal of Research and Development3(1959), no. 2, 114–125

    1959

  28. [28]

    Salomaa and M

    A. Salomaa and M. Soittola,Automata-theoretic aspects of formal power series, Text and Monographs in Computer Science, Springer, New York, 1978

    1978

  29. [29]

    M. P. Sch¨ utzenberger,On the definition of a family of automata, Information and Control 4(1961), no. 2–3, 245–270

    1961

  30. [30]

    Z. Wei, X. Zhang, Y. Zhang, and M. Sun,Weighted automata extraction and explanation of recurrent neural networks for natural language tasks, Journal of Logical and Algebraic Methods in Programming136(2023), 100907. 26 Appendices A Detailed Proofs This appendix provides detailed proofs of the main results as well as additional technical arguments omitted f...

    2023

  31. [31]

    ∈ T2; •for (i 1, i2)∈I, wt I(i1, i2) = wtI1(i1)⊗wt I2(i2); •for (f 1, f2)∈F, wt F (f1, f2) = wtF1(f1)⊗wt F2(i2); • for t = ((q1, q2), a,(q′ 1, q′ 2)) ∈T , wtT (t) = [wtT1(q1, a, q′

  32. [32]

    Note that here⊗is applied toF-expressions

    ⊗wt T2(q2, a, q′ 2)]. Note that here⊗is applied toF-expressions. It can be shown that [ [A⊗] ]= [ [A1] ]⊗[ [A2] ]. The idea is that, for each word w, there is a one-to-one correspondence between the runs of A⊗ and the pairs of runs of A1 and A2 on the same word w. By pairing states and synchronizing transitions on the same input symbol, each accepting run...

  33. [33]

    Since [ [A] ](ε) = 0, we have qI ̸= qF

    Summing over all runs then yields the Cauchy product of [ [A 1] ] and [ [A2] ] (b) Let A = (Q,{q I }, T,{q F }, [qI 7→1 ],wt T , [qF 7→1 ]). Since [ [A] ](ε) = 0, we have qI ̸= qF . We defineA ∗ fromAby merging the statesq I andq F , i.e. A∗ = (Q\ {q F },{q I }, T ′,{q I },[q I 7→1],wt ′ T ,[q I 7→1]). where: •T ′ =T ′ 1 ∪T ′ 2 such that –T ′ 1 ={(q, a, q...

  34. [34]

    By merging the initial state qI and the final state qF , every run of A∗ corresponds to a sequence of one or more runs of A concatenated end-to-end

    and, for all ( q, a, qI) ∈T ′ 2, by wtT ′(q, a, qI) = wtT (q, a, qF ). By merging the initial state qI and the final state qF , every run of A∗ corresponds to a sequence of one or more runs of A concatenated end-to-end. Each transition in A∗ that originally ended at qF now loops back to qI, so the weight of a run in A∗ is exactly the product of the weight...

  35. [35]

    ,| |qf | |E}} and, for every q′ f = (qf , i) ∈F ′, we let wtF ′(q′ f) = wtF (qf); • for every t = (p, a, q) ∈T , every ip ∈ {1,

    = wtI(q0); •F ′ = {(qf , i) |q f ∈Fandi∈ { 1, . . . ,| |qf | |E}} and, for every q′ f = (qf , i) ∈F ′, we let wtF ′(q′ f) = wtF (qf); • for every t = (p, a, q) ∈T , every ip ∈ {1, . . . ,| |p| |E} and every iq ∈ {1, . . . ,| |wtT (t)| |E}, we lett ′ = ((p, ip), a,(q, i q))∈T ′ and wtT ′(t′) = (wtT (t))(iq) E . Then, [ [AE] ]= [ [A⟨E⟩⊕] ]and hence [ [WFFAΣ...

  36. [36]

    lM i=1 ⟨ ⟨πi⟩ ⟩ # , e <0 =

    ∈S for all i∈ [k]. Then, again, by (b), e can also be replaced with an equivalent expression from⟨E⟩ ⊕. 30 These observations imply that, by modifying only transition weights, we may transform A∗ into an automaton A∗ ⟨E⟩⊕ ∈WFFA Σ,F(⟨E⟩⊕) without changing its behavior, i.e., [ [A∗ ⟨E⟩⊕ ] ]= F ∗. By Lemma 6.7, there exists an automaton A∗ E ∈WFFA Σ,F(E) wit...