Differentiable Weighted Automata

Anand Balakrishnan 1 Jyotirmoy V. Deshmukh 1

Abstract

While weighted automata are powerful tools to computequantitative costs or weights of structured input sequences —images, words, robot trajectories — they have been challenging to use in gradient-based pipelines due to their inherently
discrete structures. For example, in trajectory optimizationand control theory, automata-based techniques decompose
the optimization problem over the automaton as “sub-tasks”.
Such frameworks usually reduce to a graph game on a composition of the specification automaton and an underlying
model of the system [19], [20]; or as hierarchical hybrid systems [21]–[24]. In a similar vein, recent literature on rewardmachine-based reinforcement learning, various frameworks
learn policies for such sub-tasks. The works in [25] and [26]propose compositional approaches to learning policies for
sub-tasks in reward machines to satisfy a global task. Thesemethods are inherently restricted use to the state explosionthat happens by decomposing the automaton, and thus, don’t
scale well to more complex specifications and systems.

Weighted automata have been used extensively
for studying quantitative properties of systems,
modeling the behavior of probabilistic systems,
and various text, speech, and image processing
domains. Moreover, they have become popular
in reinforcement learning for task specificationsin the form of reward machines. This is due totheir ability to assign a quantitative score to somesequence of inputs in the problem domain. While
the weighted automaton formalism is powerful
and well-studied in literature, its inherently discrete structure makes it difficult to use in gradientbased pipelines. In this paper, we present a systematic framework for designing differentiableweighted automata that can leverage automaticdifferentiation tools to compute the gradient of
the weight calculated by a weighted automatonwith respect to its input sequence.

Our Contributions In this paper, we present a construction of weighted automata using matrix semirings that allows for the automaton to be directly deployed in neuralnetwork-based pipelines. We describe a set of necessary
conditions to construct a class of weighted automata thatcan be differentiable with respect to their inputs, thereby
leveraging state-of-the-art automatic differentiation tools[27]. Further, we present empirical results in trajectory
optimization for some sequential, time-dependent tasks.

1. Introduction
Weighted automata are a generalization of finite-state automata over algebraic semiring structures that arose fromthe connection of finite automata and rational formal power
series [1]–[3]. Here, in addition to checking if an input
sequence (or word) is accepting or rejecting, a weight isassociated with the input word and the run induced by input word in the weighted automaton. Weighted automata
have extensively been used for the verification of quantitative properties [4]–[7], for reasoning about probabilistic
systems [8], [9], and for text, speech, and image processing[10]–[13]. In recent literature on reinforcement learning, aspecialization of weighted automata — reward machines— have been introduced to express reward functions forcomplex spatiotemporal tasks [14]–[18].

While a notion of differentiable weighted automata for natural language processing has been explored in [28], [29] —over graph operations on the automata, i.e., with respect toother automata or the transitions of an automaton — ourapproach looks at an orthogonal problem. Specifically, we
study the semantics of differentiability of the weights outputted by a fixed automaton with respect to the input sequences — a common occurrence in trajectory optimization
and reinforcement learning with reward machines. To thebest of our knowledge, this is the first presentation of suchdifferentiable automata along with the conditions to construct them.

1
Thomas Lord Department of Computer Science, University ofSouthern California, Los Angeles, CA 90005, USA. Correspondence to: Anand Balakrishnan <anandbal@usc.edu>, Jyotirmoy
V. Deshmukh <jdeshmuk@usc.edu>.

2. Preliminaries

Published at the 2 nd Differentiable Almost Everything Workshop
at the 41 st International Conference on Machine Learning, Vienna, Austria. July 2024. Copyright 2024 by the author(s).

In this section, we will define some notations and provide
some background for our proposed framework.
1x 6∈ Rred ∪ Rblue
start

q0

x 6∈ Rgreen ∪ Rblue

x 6∈ Rorange ∪ Rblue

x 6∈ Rblue

q1

q2

q3

x ∈ Rredx ∈ Rgreen

bluex ∈ Rblue

R

e
lu

lue

Rb

Semirings are algebraic structures that are used to define
the semantics of non-deterministic weighted automata, defined later in this section. Important examples of semirings
include:

Rb

∈

x∈

x∈

x ∈ Rorange
xDefinition 1 (Semiring [30]). The tuple (K, ⊕, ⊗, 0̃, 1̃) is asemiring with the underlying set K if K, ⊕, 0̃ is a commutative monoid with identity 0̃; K, ⊗, 1̃ is a monoid
with identity element 1̃; ⊗ distributes over ⊕; and 0̃ is anannihilator for ⊗ (for all k ∈ K, k ⊗ 0̃ = 0̃ ⊗ k = 0̃).

q4>

Figure 1. Example of an automaton with inputs x ∈ X ⊂ Rn .
Here, for various regions Rred , Rgreen , Rorange , Rblue contained in
X , the automaton specifies a task: “move to region Rred , thenregion Rgreen , and then to region Rorange in order while always
avoiding the region Rblue .”• Boolean semiring, ({0, 1} , ∨, ∧, 0, 1) with oroperation acting as addition and and-operation acting
as multiplication;• The real numbers (R, +, ×, 0, 1) with the usual addition and multiplication.

• λ : Q × Σ × Q → K is a transition weight function,α : Q0 → K is the initial weights function and β :QF → K is the final weights function.

• The log-semiring with the extended reals(R ∪ {−∞, ∞} , ⊕log , +, −∞, 0),where
x ⊕log y = logb (bx + by ), for some base b;

As is convention, we use Σ∗ to refer to the set of all finite
length sequence of elements x ∈ Σ. Given an input sequence, ξ = (x0 , x1 , . . . , xl ) ∈ Σ∗ , a run in the symbolic
automaton A is a sequence of locations (q0 , q1 , . . . , ql+1 )such that qi+1 ∈ ∆(qi , xi ) for all i ∈ 0, . . . , l. We usexi
qi −→qi+1 to denote a valid transition in the automaton,and runA (ξ) to denote the set of runs induced in A by
ξ ∈ Σ∗ . We say that the automaton is non-deterministic
if a trace ξ can generate multiple runs in A, i.e., if forsome input x and location q, |∆(q, x)| > 1. A run is accepting in the automaton if ql ∈ QF for any induced run(q0 , q1 , . . . , ql ) ∈ runA (ξ), and we denote this by ξ |= A.
The weight of an input trace ξ = (x0 , . . . , xl ) ∈ Σ∗ on aweighted automaton A is!
l
M
OwA (ξ) =λ(qi , xi , qi+1 ) ⊗ β(ql+1 ).
α(q0 ) ⊗• Thetropicalmax-plus
semiring(R ∪ {−∞, ∞} , max , +, −∞, 0), which can bederived from the limit of log-semiring as the baseb → ∞.
The log-semiring and the tropical semiring are used extensively in the context of optimization, where the tropicalsemiring appears in shortest-path analysis (as the min-plus
semiring, which is isomorphic to the max-plus semiring via
negation). The former is used for smooth-approximationsof min and max operations, and in problems involving
log-likelihoods.
If the multiplication operation ⊗ is commutative, we saythat the semiring is also commutative, and it is said to be
idempotent if the addition operation is such that x ⊕ x = x
for all x ∈ K. All of the above described semirings arecommutative, while only the Boolean and tropical semirings
are idempotent. In the following definitions, we will use K
to denote semirings.

runA (ξ)i=0(1)
Example. Consider a 2D workspace X ⊂ R with four
regions Rred , Rgreen , Rorange , Rblue contained in X . Let
us have a robot in the workspace that is required to visit
the regions in the strict order Rred , Rgreen , Rorange , while
never entering the region Rblue . In Figure 1, we see the(unweighted) automaton describing such a task: the input
alphabet Σ = X and the expressions on the transitions(or guards) represent the condition when the transition is
feasible, i.e., when the condition is true for a transitionx→ qi+1 then qi+1 ∈ ∆(qi , x). Moreover, the location q4
qi −(with a tautology self-loop) is a rejecting sink location in theautomaton. In Figure 2, we see an example of a trajectorythat satisfies the requirement.
Definition 3 (Matrix Semirings [31]). If m is a positive
integer and K is a semiring, then the set of m × m matrices with entries in K, denoted K m×m , is also a semiring.
2

Definition 2 (Weighted Automaton [1]). A weighted automaton is a tuple A = (Σ, Q, Q0 , QF , ∆λ, α, beta),where• Σ is an input alphabet;• Q is a set of locations in the automaton, with Q0 and
QF denoting the initial and final (or accepting) locations respectively;• ∆ : Q × Σ → 2Q is a transition function, where 2Q
denotes the powerset of Q;
2

networks. Moreover, we can use arbitrarily large numbers
for semirings with ∞ to ease practical use.
Let the locations in Q an automaton A be indexed q0
through q|Q|−1 . Then, we use 1Q0 and 1QF be the Boolean|Q|
indicator vectors in {0, 1} with entries such that(0, if qi 6∈ Q0(1Q0 )i =1, if qi ∈ Q0(
0, if qi 6∈ QF(1QF )i =1, if qi ∈ QF .

Figure 2. An example trajectory in a 2D workspace that satisfies
the specification in Figure 1 described in Example 2. Here, thestate x is a vector in X ⊂ R2 , and the trajectory starts at a point(−1, −1) and completes the specified task.

Similarly, we define the initial weights α ∈ K |Q| and final
weights β ∈ K |Q| as(0̃,
if qi 6∈ Q0(α)i =α(qi ), if qi ∈ Q0(0̃,
if qi 6∈ QF(β)i =
β(qi ), if qi ∈ QF .

Specifically, for matrices A, B, C ∈ K m×m , we can define
the semiring operation as follows:• Addition A ⊕ B = C is defined as element-wise addition Cij = Aij ⊕ Bij ;Specifically, for a given weighted automaton A over a semiring K, we define alternative matrix operators A∆ : Σ →|Q|×|Q|{0, 1}and Aλ : Σ → K |Q|×|Q| , corresponding to ∆and λ respectively.

• The additive identity matrix is, intuitively, the m × m
matrix with all entries 0̃;• Multiplication AB = CLis defined similar to matrix
m−1
multiplication as Cij = k=0 Aik ⊗ Bkj ; andDefinition 4 (Transition Matrix Operator). For an automaton A, the corresponding transition matrix operator|Q|×|Q|A∆ : Σ → {0, 1}
is defined such that A∆ (x) is
an element of the |Q| × |Q| Boolean matrix semiring, theentries of which are:(0, if qj 6∈ ∆(qi , x)(A∆ (x))ij =(2)
1, if qj ∈ ∆(qi , x),• The multiplicative identity matrix (or simply, identity
matrix) is similar to the usual: an m × m matrix withall diagonal entries equal to 1̃, and the rest are 0̃.
From the above definition of matrix semiring, one can derive
the vector-dot product (x3 = x1 · x2 = x1 x2 ), and vectormatrix multiplication (x2 = xT1 A).1 We refer readers to[31] to see various other linear algebra equivalences under
the algebraic framework.

where qi and qj are locations in Q indexed from 0 to |Q| − 1.
Definition 5 (Weight Matrix Operator). For an automatonA, the corresponding weight matrix operator Aλ : Σ →K |Q|×|Q| is defined such that Aλ (x) is an element of the|Q| × |Q| K-matrix semiring, the entries of which are:

3. Differentiable Automata Operators
In this section, we will look at an alternative constructionof weighted automata as matrix operators by leveraging
extensive literature on automata theory has studied the field— especially weighted and quantitative automata — fromthe perspective of linear algebra [31]–[33].
Remark. Throughout the rest of the paper, we restrict ourselves to Σ ⊆ Rn in an effort to keep our framework relevant
to compute pipelines that rely on floating point operations.
In practice, any input alphabet can be encoded into some
vector embedding, similar to what is done in image processing, natural language processing, and with graph neural(Aλ (x))ij = λ(qi , x, qj ),(3)

where qi and qj are locations in Q indexed from 0 to |Q| − 1.
From the above and prior definitions, we can derive thefollowing results:
Lemma 1. Given an input ξ = (x0 , x1 , . . . , xl ) ∈ Σ∗ andthe function:
AccA (ξ) = 1TQ0 A∆ (x0 )A∆ (x1 ) . . . A∆ (xl )1QF ,(4)then ξ |= A if and only if AccA (ξ) = 1. Moreover, theweight wA (ξ) is given by1
We will use the standard notation for matrix operations but
defined over semirings unless otherwise specified.

wA (ξ) = αT Aλ (x0 )Aλ (x1 ) . . . Aλ (xl )β3(5)holdObj¬holdObj

Proposition 1 (Conditions for Differentiability). Given an
automaton A and a semiring K ⊆ R, the gradient of theA (ξ)
weight with respect to input sequences ξ ∈ Σ∗ , ∂w∂ξ
, iswell-defined if and only if:

start

holdObj
q0

q1>
reachGoalq2¬holdObj• a1 ⊕ a2 and a1 ⊗ a2 are differentiable at all points in
Σ, for a1 , a2 ∈ K;

Figure 3. The automaton for the Pusher environment, where an
articulated arm is used to push an object from one position to agoal location. Here, the predicate holdObj specifies that the arm
must reach/hold the object, and reachGoal specifies that the object
must reach the goal location.

• λ(q, x, q ′ ) is differentiable at all x ∈ Σ for all feasiblexq−→ q ′ transitions in A.
Example. In the example in Figure 1, by using the logsemiring with the weighting function λ(q, x, q ′ ) as the Euclidean distance of x from the regions that enable eachtransition in the automaton in Figure 1, we can obtain a differentiable wA . Moreover, since both, ⊕log and Euclidean
distance are smooth functions, we can see that optimizing
wA — a smooth function — gives an approximation of theshortest path in the system that satisfies the specification.

Table 1. Results for Gradient-based Trajectory Optimization

Environment

Epochs to satisfaction

Learning Rate

Unicycle

425

0.05

Pusher1562

0.05

4. Experimental Results
To demonstrate the use of differentiable weighted automata
as specifications for trajectory optimization, we look at theexample of two different environments. For both these environments, we use JAX [34] and Brax [35] to simulate the dynamics of the agent in the environment, and the log-semiring
to compute the weights of the trajectories. Moreover, since
we look at the log-semiring, our goal is to maximize theweights of the trajectory, as results in [36] establish that a
non-negative weight for the log-semiring is equivalent tofinding a satisfying input sequence. The results of our experiments are detailed in Table 1, where we see the numberof gradient update epochs required to find a satisfying trajectory in the environment with the corresponding learning
rate.2 We set the control inputs over the entire discretetime trajectory in both environments as the optimization
parameters.

ticulated arm to push an object from its initial location
to a goal location within 1000 time steps (at a period of
0.05 seconds). The automaton in Figure 3 describes thisspecification, where the predicates holdObj and reachGoal
correspond to the task for the arm reaching and holding theobject, and then subsequently for the object to reach thegoal. To make the task of “reaching” a location feasible, we
describe them as follows:
holdObjreachGoal⇐⇒⇐⇒∥parm − pobj ∥ ≤ 0.005m∥pobj − pgoal ∥ ≤ 0.005m,

where parm , pobj , and pgoal are the 3D coordinates of theend of the arm, the object, and the goal position, respectively.
Moreover, for each transition guard in the automaton, wepick the weight function λ to be as follows:
holdObj : λ(·, x, ·) = −max(0, ∥parm − pobj ∥ − 0.005)¬holdObj : λ(·, x, ·) = −max(0, 0.005 − ∥parm − pobj ∥)reachGoal : λ(·, x, ·) = −max(0, ∥pobj − pgoal ∥ − 0.005)> : λ(·, x, ·) = 0̃ = −∞Unicycle We perform control of a second-order unicycle
model on a 2-dimensional workspace, where the state vectorof the agent consists of the position, heading, velocity, andangular velocity; we control the linear and angular acceleration of the unicycle; and the task at hand is the sequential
reach-avoid automaton in Figure 1. For each transition
guard on the automaton, the distance function λ computes
the distance from the current position of the unicycle to thecondition regions. The system is sampled at 0.1 second rate
for a trajectory of length 80 time steps (or 8 seconds).

5. Conclusion
In this paper, we present a framework for designing differentiable weighted automata. To the best of our knowledge,
this is the first such paper to propose a set of necessary conditions for differentiability of a weighted automaton output
with respect to the input sequence. We present an initial
set of experiments to demonstrate the use of our framework
in a gradient-based trajectory optimization problem, both
examples being non-linear systems with sequential tasks.

Pusher The Pusher environment in Brax [35] is a 23dimensional system where we control a multi-jointed ar2

As these environments don’t have highly non-convex objectives, simple gradient ascent is sufficient, but, in general, one mustchoose an appropriate optimizer and set of hyperparameters.

4

References
[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

M. Droste, W. Kuich, and H. Vogler, Eds., Handbook of
Weighted Automata (Monographs in Theoretical Computer
Science. An EATCS Series). Berlin, Heidelberg: Springer
Berlin Heidelberg, 2009, ISBN: 978-3-642-01492-5. DOI:
10.1007/978-3-642-01492-5.
U. Boker, “Quantitative vs. Weighted Automata,” in Reachability Problems, P. C. Bell, P. Totzke, and I. Potapov, Eds.,
vol. 13035, Cham: Springer International Publishing, 2021,
pp. 3–18, ISBN: 978-3-030-89716-1. DOI: 10 . 1007 /978-3-030-89716-1_1.
A. Salomaa and M. Soittola, Automata-Theoretic Aspects ofFormal Power Series. New York, NY: Springer New York,
1978, ISBN: 978-1-4612-6264-0. DOI: 10.1007/9781-4612-6264-0.
K. Chatterjee, L. Doyen, and T. A. Henzinger, “Alternating
Weighted Automata,” in Fundamentals of Computation
Theory, M. Kutyłowski, W. Charatonik, and M. G˛ebala,Eds., Berlin, Heidelberg: Springer, 2009, pp. 3–13, ISBN:
978-3-642-03409-1. DOI: 10 . 1007 / 978 - 3 - 642 03409-1_2.
K. Chatterjee, T. A. Henzinger, and J. Otop, “Quantitative
Automata under Probabilistic Semantics,” in Proceedingsof the 31st Annual ACM/IEEE Symposium on Logic in
Computer Science, ser. LICS ’16, New York, NY, USA: Association for Computing Machinery, Jul. 2016, pp. 76–85,
ISBN : 978-1-4503-4391-6. DOI : 10.1145/2933575.
2933588.
M. Droste and P. Gastin, “Weighted Automata andWeighted Logics,” Theoretical Computer Science, Automata, Languages and Programming, vol. 380, no. 1,
pp. 69–86, Jun. 2007, ISSN: 0304-3975. DOI: 10.1016/
j.tcs.2007.02.055.
R. Alur, L. D’Antoni, J. V. Deshmukh, M. Raghothaman,
and Y. Yuan, Regular Functions, Cost Register Automata,and Generalized Min-Cost Problems, Feb. 2012. DOI: 10.
48550 / arXiv . 1111 . 0670. arXiv: 1111 . 0670
[cs].
K. Chatterjee, L. Doyen, and T. A. Henzinger, “Probabilistic Weighted Automata,” in CONCUR 2009 - Concurrency
Theory, M. Bravetti and G. Zavattaro, Eds., Berlin, Heidelberg: Springer, 2009, pp. 244–258, ISBN: 978-3-64204081-8. DOI: 10.1007/978-3-642-04081-8_17.
S. Adhikary, S. Srinivasan, J. Miller, G. Rabusseau, and B.
Boots, “Quantum Tensor Networks, Stochastic Processes,
and Weighted Automata,” in Proceedings of The 24th International Conference on Artificial Intelligence and Statistics,
PMLR, Mar. 2021, pp. 2080–2088.
K. Knight and J. Graehl, “An Overview of Probabilistic Tree Transducers for Natural Language Processing,”
in Computational Linguistics and Intelligent Text Processing, D. Hutchison, T. Kanade, J. Kittler, et al., Eds.,
vol. 3406, Berlin, Heidelberg: Springer Berlin Heidelberg, 2005, pp. 1–24, ISBN: 978-3-540-30586-6. DOI: 10.
1007/978-3-540-30586-6_1.
K. Knight and J. May, “Applications of Weighted Automata
in Natural Language Processing,” in Handbook of Weighted
Automata, M. Droste, W. Kuich, and H. Vogler, Eds., Berlin,
Heidelberg: Springer Berlin Heidelberg, 2009, pp. 571–
596, ISBN: 978-3-642-01492-5. DOI: 10.1007/978-3642-01492-5_14.

[13]

[14]

[15]

[16]

[17]

[18]

[19]
[20]

[21]

[22]

[23]

5

M. Mohri, F. Pereira, and M. Riley, Weighted Automata in
Text and Speech Processing, Mar. 2005. DOI: 10.48550/
arXiv.cs/0503077. arXiv: cs/0503077.
K. Culik and J. Kari, “Image Compression Using Weighted
Finite Automata,” Computers & Graphics, vol. 17, no. 3,
pp. 305–313, May 1993, ISSN: 0097-8493. DOI: 10 .
1016/0097-8493(93)90079-O.
R. T. Icarte, T. Klassen, R. Valenzano, and S. McIlraith,“Using Reward Machines for High-Level Task Specification and Decomposition in Reinforcement Learning,” inProceedings of the 35th International Conference on Machine Learning, PMLR, Jul. 2018, pp. 2107–2116. [Online].
Available: https://proceedings.mlr.press/
v80/icarte18a.html.
R. Toro Icarte, E. Waldie, T. Klassen, R. Valenzano, M. Castro, and S. McIlraith, “Learning Reward Machines for Partially Observable Reinforcement Learning,” in Advancesin Neural Information Processing Systems, vol. 32, Curran Associates, Inc., 2019. [Online]. Available: https:/ / proceedings . neurips . cc / paper / 2019 /hash / 532435c44bec236b471a47a88d63513d Abstract.html.
A. Camacho, R. Toro Icarte, T. Q. Klassen, R. Valenzano,and S. A. McIlraith, “LTL and Beyond: Formal Languages
for Reward Function Specification in Reinforcement Learning,” in Proceedings of the Twenty-Eighth International
Joint Conference on Artificial Intelligence, Macao, China:
International Joint Conferences on Artificial Intelligence
Organization, Aug. 2019, pp. 6065–6073, ISBN: 978-09992411-4-1. DOI: 10.24963/ijcai.2019/840.
J. Corazza, I. Gavran, and D. Neider, “Reinforcement
Learning with Stochastic Reward Machines,” Proceedingsof the AAAI Conference on Artificial Intelligence, vol. 36,
no. 6, pp. 6429–6436, Jun. 2022, ISSN: 2374-3468. DOI:
10.1609/aaai.v36i6.20594.
A. Balakrishnan, S. Jakšić, E. A. Aguilar, D. Ničković, andJ. V. Deshmukh, “Model-Free Reinforcement Learning for
Spatiotemporal Tasks Using Symbolic Automata,” in 2023
62nd IEEE Conference on Decision and Control ( CDC),
Dec. 2023, pp. 6834–6840. DOI: 10.1109/CDC49753.
2023.10383559.
C. Baier and J.-P. Katoen, Principles of Model Checking.
MIT Press, Apr. 2008, ISBN: 978-0-262-30403-0.
T. Wongpiromsarn, U. Topcu, and R. M. Murray, “Receding Horizon Temporal Logic Planning,” IEEE Transactions
on Automatic Control, vol. 57, no. 11, pp. 2817–2830, Nov.
2012, ISSN: 1558-2523. DOI: 10 . 1109 / TAC . 2012 .
2195811.
H. Kress-Gazit, G. E. Fainekos, and G. J. Pappas,“Temporal-Logic-Based Reactive Mission and Motion Planning,” IEEE Transactions on Robotics, vol. 25, no. 6,
pp. 1370–1381, Dec. 2009, ISSN: 1941-0468. DOI: 10 .
1109/TRO.2009.2030225.
G. E. Fainekos, A. Girard, H. Kress-Gazit, and G. J. Pappas,“Temporal Logic Motion Planning for Dynamic Robots,”
Automatica, vol. 45, no. 2, pp. 343–352, Feb. 2009, ISSN:
0005-1098. DOI: 10.1016/j.automatica.2008.
08.008.
S. L. Smith, J. Tůmová, C. Belta, and D. Rus, “Optimal
Path Planning for Surveillance with Temporal-Logic Constraints,” The International Journal of Robotics Research,
vol. 30, no. 14, pp. 1695–1708, Dec. 2011, ISSN: 02783649. DOI: 10.1177/0278364911417911.

[24]

[25]

[26]

[27]

[28]

[29]

[30]

[31]

[32]

[33]

[34]

[35]

[36]

L. Lindemann and D. V. Dimarogonas, “Efficient
Automata-based Planning and Control under SpatioTemporal Logic Specifications,” in 2020 American Control Conference (ACC), Jul. 2020, pp. 4707–4714. DOI:
10.23919/ACC45564.2020.9147796.
K. Jothimurugan, R. Alur, and O. Bastani, “A composable specification language for reinforcement learning
tasks,” Advances in Neural Information Processing Systems, vol. 32, 2019.
L. Illanes, X. Yan, R. T. Icarte, and S. A. McIlraith, “Symbolic Plans as High-Level Instructions for Reinforcement
Learning,” Proceedings of the International Conference on
Automated Planning and Scheduling, vol. 30, pp. 540–
550, Jun. 2020, ISSN: 2334-0843. [Online]. Available:
https://ojs.aaai.org/index.php/ICAPS/
article/view/6750.
A. G. Baydin, B. A. Pearlmutter, A. A. Radul, and J. M.
Siskind, “Automatic Differentiation in Machine Learning:
A Survey,” Journal of Machine Learning Research, vol. 18,
no. 153, pp. 1–43, 2018, ISSN: 1533-7928. [Online]. Available: http://jmlr.org/papers/v18/17- 468.
html.
A. Hannun, V. Pratap, J. Kahn, and W.-N. Hsu. “Differentiable Weighted Finite-State Transducers.” arXiv: 2010.
01003 [cs, stat]. (Oct. 2, 2020), preprint.
A. Hannun, “An Introduction to Weighted Automata in
Machine Learning,” 2021. [Online]. Available: https:/ / awnihannun . com / writing / automata _ ml /automata_in_machine_learning.pdf.
M. Mohri, “Semiring Frameworks and Algorithms for
Shortest-Distance Problems,” Journal of Automata, Languages and Combinatorics, vol. 7, no. 3, pp. 321–350, Jan.
2002, ISSN: 1430-189X.
J. S. Golan, Semirings and Affine Equations over Them:
Theory and Applications. Dordrecht: Springer Netherlands,
2003, ISBN: 978-94-017-0383-3. DOI: 10.1007/97894-017-0383-3.
W. Kuich and A. Salomaa, Semirings, Automata, Languages. Berlin, Heidelberg: Springer Berlin Heidelberg,
1986, ISBN: 978-3-642-69959-7.
M. Mohri, “Weighted Automata Algorithms,” in Handbookof Weighted Automata, M. Droste, W. Kuich, and H. Vogler,Eds., Berlin, Heidelberg: Springer Berlin Heidelberg, 2009,
pp. 213–254, ISBN: 978-3-642-01492-5. DOI: 10.1007/
978-3-642-01492-5_6.
R. Frostig, M. J. Johnson, and C. Leary, “Compiling machine learning programs via high-level tracing,” Systems
for Machine Learning, vol. 4, no. 9, 2018. [Online]. Available: https://mlsys.org/Conferences/doc/
2018/146.pdf.
C. D. Freeman, E. Frey, A. Raichuk, S. Girgin, I. Mordatch,and O. Bachem, Brax – A Differentiable Physics Engine forLarge Scale Rigid Body Simulation, Jun. 2021. DOI: 10.
48550/arXiv.2106.13281. arXiv: 2106.13281[cs].
S. Jakšić, E. Bartocci, R. Grosu, and D. Ničković, “AnAlgebraic Framework for Runtime Verification,” IEEE
Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 37, no. 11, pp. 2233–2243, Nov.
2018, ISSN: 1937-4151. DOI: 10.1109/TCAD.2018.
2858460.

6