Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

July 28, 2022

Compositional Constructions of Automata

Posted by Emily Riehl

guest post by Ruben van Belle and Miguel Lopez

In this post we will detail a categorical construction of automata following the work of Albasini, Sabadini, and Walters. We first recall the basic definitions of various automata, and then outline the construction of the aformentioned authors as well as generalizations and examples.

A finite deterministic automaton consists of

  • a finite set QQ (state space),

  • an initial state q 0Xq_0\in X and a set FQF\subseteq Q of accepting states,

  • a finite set AA of input symbols and a transition map τ a:QQ\tau_a:Q\to Q for every aAa\in A.

Imagine a frog in pond with a 100100 lily pads, which form a 1010 by 1010 grid. Suppose that the frog sits on a lily pad and can only make jumps of one unit i.e. the frog can jump forwards, backwards, left or right.

Let QQ be the set of lily pads. Let q 0q_0 be the lily pad the frog currently is sitting on and let q 1q_1 be the lily pad the frog wants to go to. Let AA be the set of symbols {f,b,l,r}\{f,b,l,r\}. A jump forward corresponds to an input of ff and to the map τ f:QQ\tau_f:Q\to Q moving the frog forward (if possible) in the grid. Similarly, the symbols b,lb,l and rr with respective maps τ b,τ l\tau_b,\tau_l and τ r\tau_r correspond to jumps backwards, left and right, whenever these are possible. The data (Q,q 0,{q 1},A,(τ a) aA)(Q,q_0,\{q_1\},A, (\tau_a)_{a\in A}) form a finite deterministic automaton.

The transition maps in the definition of a finite deterministic automaton are morphisms in FinSet\mathbf{FinSet}, the category of finite sets and functions. We can generalize the idea of a finite deterministic automaton, by letting the transition maps be morphisms in more general categories. In particular we will look at Kleisli categories of monads on FinSet\mathbf{FinSet} or Set\mathbf{Set}.

If the transition map is a map in the Kleisli category of the powerset monad, i.e. functions M a:Q𝒫(Q)M_a:Q\to\mathcal{P}(Q), we obtain finite non-deterministic automata. In our example that would mean that the frog can choose between a set of different jumps for a given input. If the frog is sitting on lily pad qq, then τ f(q)\tau_f(q) is the set of all reachable lily pads that are in front of the frog.

If we let the transition map be a morphism in the Kleisli category of the monad of finitely supported measures on Set\mathbf{Set}, we obtain weighted automata and if the transition map is a morphism in the Kleisli category of the distribution monad, we obtain Markov automata. In the case of the frog this would mean that the frog prefers some lily pads over others and this preference is given in terms of distributions. If the frog sits on lilypad qq, then τ f(q)\tau_f(q) is a distribution on the reachable lily pads in front of the frog.

In the following, we will first consider categories of Markov automata as presented in The compositional construction of Markov process II by Albasini, Sabadini, and Walters and then generalize this to TT-automata for commutative strong monads TT on a monoidal category 𝒞\mathcal{C}. We will study categories where the morphisms are these generalized automata and look at the monoidal structure and properties this category inherits from 𝒞\mathcal{C} and 𝒞 T\mathcal{C}_T.

Markov Automata

Here, we will consider a definition of automata that deviates from the classical literature. A Markov automaton Q Y;A,B XQ^X_{Y;A,B} consists of the following data:

  • A set of states also denoted QQ.

  • Two sets of parallel interfaces AA and BB (playing the role of inputs/signals)

  • Two sets of sequential interfaces XX and YY together with functions γ Q:XQ\gamma_Q:X\to Q and δ Q:YQ\delta_Q:Y\to Q in 𝒞\mathcal{C} (playing the role of start/stop states)

  • Transition matrices indexed by the parallel interfaces Q a,bQ_{a,b} such that for all qQq \in Q qQ aA,bBQ a,b=1 \sum_{q'\in Q} \sum_{a\in A, b\in B} Q_{a,b} = 1

Markov automata form a symmetric monoidal category in two distinctly different ways: one in which we compose automata in parallel and one in which we compose in sequence.

Parallel Composition

Let ParAut\mathbf{ParAut} be the category with

  • objects as finite sets A,B,C,A,B,C,\dots

  • morphisms ABA \to B as weighted automata whose parallel interfaces are the sets AA and BB.

The parallel composite of morphisms ABCA \to B \to C is defined to be the weighted automaton with states Q×RQ \times R and whose top and bottom interfaces are the respective set products X×ZX \times Z and Y×WY \times W with sequential interface functions γ Q×γ R\gamma_Q \times \gamma_R and δ Q×δ R\delta_Q \times \delta_R. The parallel interfaces are AA and CC with transition matrices defined by

(Q||R) a,c= bBQ a,bR b,c (Q||R)_{a,c} = \sum_{b\in B} Q_{a,b} \otimes R_{b,c}

where \otimes denotes the Kronecker product of matrices. This is shown diagrammatically in the figure below.

Parallel Composition.

The tensor product of two objects AA and BB in ParAut\mathbf{ParAut} is their cartesian product A×BA\times B. On morphisms Q Y;A,B XQ^X_{Y;A,B} and R W;C,D ZR^Z_{W;C,D}, the tensor product has as states Q×RQ \times R, transition matrices

(Q×R) (a,c),(b,d)=Q a,bR c,d, (Q \times R)_{(a,c),(b,d)} = Q_{a,b} \otimes R_{c,d},

and X×ZX \times Z and Y×WY \times W as sequential interfaces with interface functions γ Q×γ R\gamma_Q \times \gamma_R and δ Q×δ R\delta_Q \times \delta_R respectively. Note that the identity object I={*}I = \{ *\} is the one element set.

The tensor product in ParAut.

To show ParAut\mathbf{ParAut} is symmetric, we will use the fact that there is a monoidal functor

Par:RelParAut \text{Par} : \mathbf{Rel} \to \mathbf{ParAut}

on the symmetric monoidal category of (finite) sets and relations Rel\mathbf{Rel}. This functor acts as the identity on objects Par(A)=A\text{Par}(A) = A and on morphisms RA×BR \subseteq A \times B by associating RR to the following automaton:

  • Each of the sequential interfaces and state space are the singleton set X=Y=Q={*}X=Y=Q=\{*\}.

  • The left and right parallel interfaces are AA and BB respectively and the transition matrices (in this case numbers) are given by Par(R)(a,b) *,*={1, (a,b)R 0, otherwise \text{Par}(R)(a,b)_{\ast,\ast} = \begin{cases} 1, & (a,b) \in R \\ 0, & \text{otherwise} \end{cases}

for aAa \in A and bBb \in B. Symmetry in ParAut\mathbf{ParAut} then follows from Par\text{Par} being a monoidal functor. Using this technology we will show some nice properties of ParAut\mathbf{ParAut} by pushing them forward through Rel\mathbf{Rel}.

Proposition. ParAut\mathbf{ParAut} is compact closed.

This in particular allows us to define the notion of feedback. To show that Rel\mathbf{Rel} (and hence ParAut\mathbf{ParAut}) is compact closed we instead show that each object in Rel\mathbf{Rel} is a Frobenius algebra and apply the following lemma.

Lemma. If an object AA in a monoidal category forms a Frobenius algebra then it is dual to itself.

Let Δ A:AA×A\Delta_A : A \to A \times A be the diagonal map, thought of as a morphism in Rel\mathbf{Rel} and p A:A1p_A : A \to 1 the unique morphism to the terminal object. Moreover given a morphism RR, let R opR^{\text{op}} denote the opposite relation (by simply reversing the arrow). Then the monoid structure for the Frobenius algebra of an object AA in Rel\mathbf{Rel} is given by (A,Δ A op,p A op)(A,\Delta_A^{\text{op}},p_A^{\text{op}}) and, dually, the comonoid structure by (A,Δ A,p A)(A, \Delta_A,p_A).

Sequential Composition

Let SeqAut\mathbf{SeqAut} be the category with

  • objects as finite sets X,Y,ZX,Y,Z \dots

  • morphisms XYX \to Y as weighted automata

Q Y;A,B XQ^X_{Y;A,B} whose sequential interfaces are the sets XX and YY.

We define the sequential composite of two morphisms Q Y;A,B XQ^X_{Y;A,B} and R Z;C,D YR^Y_{Z;C,D} to be the weighted automaton QRQ \circ R whose states are given by the disjoint union (Q+R)/(Q + R)/\sim quotiented by the relation δ Q(y)γ R(y)\delta_Q(y) \sim \gamma_R(y). The parallel interfaces are A+CA+C and B+DB+D and top and bottom interfaces are XX and ZZ with the respective interface functions

γ :XQQ+R(Q+R)/ δ :ZRQ+R(Q+R)/.\begin{array}{cc} \gamma &: X \to Q \to Q + R \to (Q+R)/\sim \\ \delta &: Z \to R \to Q + R \to (Q+R)/\sim. \end{array}

If we let q,qQq,q' \in Q and r,rRr,r' \in R and [s][s] denote the equivalence class of state ss in Q+RQ + R, then the transition matrices are given by

[(QR) a,b] [q],[q] = s[q],s[q][Q a,b] s,s [(QR) c,d] [r],[r] = s[q],s[q][Q a,b] s,s \begin{array}{cc} [(Q \circ R)_{a,b}]_{[q],[q']} &= \sum_{s \in[q], s'\in [q']} [Q_{a,b}]_{s,s'} \\ [(Q \circ R)_{c,d}]_{[r],[r']} &= \sum_{s \in[q], s'\in [q']} [Q_{a,b}]_{s,s'} \end{array}

where all other entries are zero. This is shown diagrammatically below.

Sequential Composition.

The tensor product of Q Y;A,B XQ^X_{Y;A,B} and R W;C,D ZR^Z_{W;C,D} has states Q+RQ + R without any quotienting. The parallel interfaces are again A+CA+C and B+DB+D while top and bottom interfaces X+ZX + Z and Y+WY + W have interface functions γ Q+γ R\gamma_Q + \gamma_R and δ Q+δ R\delta_Q + \delta_R. The transition matrices are given by [(Q+R) a,b] q,q =[Q a,b] q,q [(Q+R) c,d] [r],[r] =[Q c,d] r,r \begin{array}{cc} [(Q + R)_{a,b}]_{q,q'} &= [Q_{a,b}]_{q,q'} \\ [(Q + R)_{c,d}]_{[r],[r']} &= [Q_{c,d}]_{r,r'} \end{array} where all other entries are again zero.

The tensor product in SeqAut.

Just as in the case of ParAut\mathbf{ParAut}, one can show SeqAut\mathbf{SeqAut} is a compact closed symmetric monoidal category by defining a monoidal functor Seq:RelSeqAut\text{Seq} : \mathbf{Rel} \to \mathbf{SeqAut}.

TT-Automata

We now generalize the preceding categories to work with a commutative strong monad. Let (𝒞,,I)(\mathcal{C},\otimes,I) be a (strict) symmetric monoidal category and let (T,μ,η)(T,\mu,\eta) be a commutative monad on 𝒞\mathcal{C} with strength σ\sigma. Let 𝒞 T\mathcal{C}_T be the Kleisli category of this monad. The strength induces a monoidal structure on 𝒞 T\mathcal{C}_T (see Folklore: Monoidal kleisli categories). We will denote the tensor product and unit object on 𝒞 T\mathcal{C}_T also by \otimes and II.

Definition. A TT-automaton consists of

  • an object QQ in 𝒞\mathcal{C},

  • morphisms γ Q:XQ\gamma_Q:X\to Q and δ Q:YQ\delta_Q:Y\to Q in 𝒞\mathcal{C} (sequential interfaces) and

  • objects AA and BB in 𝒞\mathcal{C} (parallel interfaces) together with a map M Q:QAQBM_Q:Q\otimes A\rightsquigarrow Q\otimes B in 𝒞 T\mathcal{C}_T (transition morphisms).

Parallel composition

Consider two TT-automata 𝒬:=(Q,γ Q,δ Q,M Q:QAQB)\mathcal{Q}:=(Q,\gamma_Q,\delta_Q,M_Q:Q\otimes A\rightsquigarrow Q\otimes B) and :=(R,γ R,δ R,M R:RBRC)\mathcal{R}:=(R,\gamma_R,\delta_R,M_R:R\otimes B\rightsquigarrow R\otimes C).

The parallel composite of \mathcal{R} and 𝒬\mathcal{Q} is given by the TT-automaton 𝒬 p:=(QR,γ Qγ R,δ Rδ Q,(1 RM Q)(1 QM R)),\mathcal{Q}\circ_p\mathcal{R}:=\big(Q\otimes R,\gamma_Q\otimes \gamma_R,\delta_R\otimes \delta_Q, (1_R\otimes M_Q)\diamond (1_Q\otimes M_R)\big), where \diamond is used to mean composition in 𝒞 T\mathcal{C}_T.

Let ParAut(T)\mathbf{ParAut}(T) be the category that has the same objects as 𝒞\mathcal{C} and where a morphism from AA to BB is a TT-automaton whose parallel interfaces are given by AA and BB and where composition is given by parallel composition.

Given two TT-automata 𝒬:=(Q;γ Q,δ Q,M Q:QAQB)\mathcal{Q}:=(Q;\gamma_Q,\delta_Q,M_Q:Q\otimes A\rightsquigarrow Q\otimes B) and :=(R,γ R,δ R,M R:RCRD\mathcal{R}:=(R,\gamma_R,\delta_R,M_R:R\otimes C \rightsquigarrow R\otimes D, we can form a new TT-automaton 𝒬 p:=(QR,γ Qγ R,δ Rδ Q,M QM R),\mathcal{Q}\otimes_p\mathcal{R}:=(Q\otimes R, \gamma_Q\otimes \gamma_R,\delta_R\otimes \delta_Q, M_Q\otimes M_R), which we call the parallel tensor product. The parrallel tensor product p\otimes_p together with the object II define a monoidal structure on ParAut(T)\mathbf{ParAut}(T).

We will now define a (strict) monoidal functor Par:𝒞 TParAut(T)\text{Par}:\mathcal{C}_T\to \mathbf{ParAut}(T) The functor acts as the identity on objects and sends a morphism ABA\rightsquigarrow B in 𝒞\mathcal{C} to the TT-automaton (I,Id I,Id I,Id If).(I,\text{Id}_I,\text{Id}_I, \text{Id}_I\otimes f).

Because the monoidal structure on 𝒞\mathcal{C} is symmetric, so is the monoidal structure on ParAut(T)\mathbf{ParAut}(T) using the monoidal functor Par\text{Par}.

Note that Par\text{Par} sends Frobenius algebras to Frobenius algebras and is surjective on objects.

Proposition. If 𝒞 T\mathcal{C}_T is compact closed, so is ParAut(T).\mathbf{ParAut}(T).

Remark. We have tried to also generalize the sequential operations to TT-automata, but we will leave the details of this construction for future work.

Examples

Consider the following game in a casino: the player is asked to place a bet, let’s say the player decides to place a bet of £aa. After the bet is placed, the dealer blindly picks a coin from a bag of (fair and unfair) coins; suppose the dealer picks coin bb, which has probability pp on heads. Then the dealer flips the coin. If coin lands on heads, the player wins £aa. If it falls on tails, the player loses the placed bet of £aa.

We represent the bank balance of the player by Q:={0,1,,N}Q:=\{0,1,\ldots, N\}. We furthermore suppose that the player enters the casino with £xx and has decided to leave the casino when their bank balance reaches states in YQY\subseteq Q.

If we let AA to be the set of possible bets, i.e. A:={0,1,,N}A:=\{0,1,\ldots,N\} and let BB be the bag of coins the dealer picks from. For a coin bBb\in B, we denote the probability on heads by p bp_b. For a bet aAa\in A and a bank balance of qq such that qaq\geq a, let M(a,q)M(a,q) be the measure on B×QB\times Q defined by (b,q){p b if q=q+a 1p b if q=qa 0 otherwise.(b,q')\mapsto \begin{cases}p_b & \text{ if }q'=q+a\\ 1-p_b & \text{ if }q'=q-a\\ 0 & \text{ otherwise.}\end{cases} This measures the chance of moving from a bank balance of qq to a balance of qq' when playing the game.

For a bet aa and a bank balance of qq such that q<aq &lt; a, let M(a,q)M(a,q) be the measure on B×QB\times Q defined by

(b,q){1 if q=q 0 otherwise,(b,q')\mapsto \begin{cases}1 & \text{ if }q=q'\\ 0 & \text{ otherwise,}\end{cases}

as the player is not allowed to bet more money than they have.

This defines the Kleisli map Q×AQ×BQ\times A\rightsquigarrow Q\times B and the data (Q,x,Y,M)(Q,x,Y,M) form a weighted automaton. Note that 0Q0\in Q is a so called deadlock state, since the player’s bank balance won’t change anymore after reaching 00. In particular, if 00 is not an element of YY, the player will have to keep playing the game forever.

Suppose now that the casino has multiple tables with different bags of coins and suppose that two friends go to the casino together. Then parallel compositions combines the information of the two friends playing at the same table, i.e. the game is played with the same coin. The parallel product and the sequential sum both combine the information of the two friends playing at different tables. The product measures the chance that person 1 reaches state qq' and that person 2 reaches state rr', while the sum measures the chance that that person 1 reaches state qq' or that person 2 reaches state rr'.

If the player starts with £xx and decides to move to a different table when reaching £yy and to stop playing when their bank balance is £zz, we can model the combination of the two games with the sequential composition.

Posted at July 28, 2022 6:24 PM UTC

TrackBack URL for this Entry:   https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/3412

2 Comments & 0 Trackbacks

Re: Compositional Constructions of Automata

Diagram links don’t work

Appending .png to them brings up a page with the picture.

Posted by: Samuel Craig on September 3, 2022 9:29 PM | Permalink | Reply to this

Re: Compositional Constructions of Automata

Thanks. I’ve fixed them.

Posted by: Tom Leinster on September 5, 2022 9:54 PM | Permalink | Reply to this

Post a New Comment