PaperlayerView exact revision on arXiv

Source-linked AI summary

Generalizing determinization from automata to coalgebras

Alexandra Silva, Filippo Bonchi, Marcello Bonsangue, Jan Rutten

arXiv:1302.1046v2cs.LO

TL;DR

Coalgebraic determinization offers a general framework for automata with structured state spaces, where the usual powerset construction is one motivating case. The paper develops a monad-based construction and demonstrates it across automata examples, including pushdown automata, while recovering behavioural equivalences. One scope boundary is that structured Moore automata cannot model Turing machines when transitions must consume input symbols.

  • Problem

    Automata with different transition structures call for a uniform account of their constructions and the behaviours used to compare their states.

    Source: Introduction · p. 2, §3 · p. 7

  • Method

    The paper generalizes determinization by structuring state spaces with a monad T and transforming FT-coalgebras into F-coalgebras when suitable conditions hold.

    Source: Introduction · p. 3

  • Results

    The framework treats multiple automata variations, characterizes pushdown automata coalgebraically, and recovers behavioural equivalences including failure and ready semantics.

    Source: §6 · p. 21

  • Takeaways & Limitations

    For the considered FT-coalgebras, the framework proves general equivalence properties, including that N-equivalent nondeterministic-automaton states are also language-equivalent.

    Source: Introduction · p. 3

    Structured Moore automata cannot model Turing machines when transitions must consume input symbols, since deciding acceptance then takes exactly the input length in steps.

    Source: §3.2 · p. 13

Abstract

from arXiv · show

The powerset construction is a standard method for converting a nondeterministic automaton into a deterministic one recognizing the same language. In this paper, we lift the powerset construction from automata to the more general framework of coalgebras with structured state spaces. Coalgebra is an abstract framework for the uniform study of different kinds of dynamical systems. An endofunctor F determines both the type of systems (F-coalgebras) and a notion of behavioural equivalence (~_F) amongst them. Many types of transition systems and their equivalences can be captured by a functor F. For example, for deterministic automata the derived equivalence is language equivalence, while for non-deterministic automata it is ordinary bisimilarity. We give several examples of applications of our generalized determinization construction, including partial Mealy machines, (structured) Moore automata, Rabin probabilistic automata, and, somewhat surprisingly, even pushdown automata. To further witness the generality of the approach we show how to characterize coalgebraically several equivalences which have been object of interest in the concurrency community, such as failure or ready semantics.

Introduction

The paper generalizes automata determinization to coalgebras whose state spaces are structured by monads, giving a uniform account of constructions and behavioural equivalences. It investigates when this approach applies and illustrates it with automata examples, including pushdown automata.

Introduction

  • Coalgebra supplies the general setting: a functor F specifies system structure and determines F-behavioural equivalence, with final coalgebras representing behaviour when they exist.The paper uses this setting to relate automata constructions and their equivalences.Source: Introduction · p. 2
  • A monad T structures states so an FT-coalgebra can be transformed into an F-coalgebra, unifying constructions such as nondeterministic determinization and partial-automaton totalization.The paper investigates conditions ensuring that a map X → F(T(X)) induces a suitable map T(X) → F(T(X)).Source: Introduction · pp. 2–3
  • The framework provides a uniform treatment of existing and new automata variations and proves general properties, including that N-behavioural equivalence implies D-language equivalence for nondeterministic automata.For nondeterministic automata, N-behavioural equivalence coincides with Park–Milner bisimilarity.Source: Introduction · p. 3
  • The paper extends an earlier conference version with proofs and examples, and adds the coalgebraic characterization of pushdown automata and the material in Section 5.Section 5 recovers equivalences including failure and ready semantics.Source: Introduction · p. 3

1. Background

This section establishes notation and the coalgebraic and algebraic foundations used later. Coalgebras encode state dynamics and behavioural equivalence, while monads and their algebras provide a way to structure state spaces.

1. Background

  • The preliminaries use Pω(X) for finite subsets, Dω(X) for finite-support full-probability distributions, and A* for words over an alphabet A.The empty word is ε, and word concatenation is denoted by · or juxtaposition.Source: §1 · p. 3

1.1. Coalgebras.

  • An F-coalgebra is a state set X with a map X → F(X) encoding its dynamics; states are behaviourally equivalent when their unique maps to a final coalgebra agree.For weak-pullback-preserving functors, behavioural equivalence coincides with bisimilarity.Source: §1.1 · pp. 3–4

1.2. Algebras.

  • A monad T has a unit and multiplication, and its algebras provide carriers with operations T(X) → X; Kleisli extension lifts maps into T(Y) to maps T(X) → T(Y).Examples include finite powersets for nondeterminism, 1 + X for partiality, and Dω for full-probability distributions.Source: §1.2 · p. 4

2. Motivating examples

The motivating examples show two ways to recover deterministic language behaviour from automata with different transition structures. Nondeterministic automata use powerset states, while partial automata add a sink state to totalize undefined transitions.

2. Motivating examples

  • The section presents nondeterministic determinization and partial-automaton totalization as motivating instances of a later general construction.Source: §2 · p. 5

2.1. Non-deterministic automata.

  • Determinization replaces an NDA's state space X with Pω(X), and the language of a singleton state in the resulting deterministic automaton matches that of the original state.More generally, a subset state's language is the union of the languages of its constituent states.Source: §2.1 · p. 5

2.2. Partial automata.

  • Totalization adds a sink state for undefined transitions, preserving each original state's language while the sink recognizes the empty language.The resulting automaton has state space 1 + X.Source: §2.2 · p. 6

3. Algebraically structured coalgebras

This section models systems with dynamics specified by a functor and state spaces structured by a monad, and defines an equivalence that absorbs the monad’s effect. It applies the framework to partial Mealy machines, structured Moore automata, and pushdown automata, and models context-free grammars coalgebraically, noting that equivalent accepted languages do not guarantee behavioural equivalence of their associated Moore automata.

3. Algebraically structured coalgebras

  • Coalgebras X → FT(X) combine transition type F with monad T, and extend uniquely to T-algebra morphisms on the structured state space T(X).The extension f♯: T(X) → FT(X) extends the original coalgebra to T(X).Source: §3 · pp. 6–7
  • The new T-relative equivalence compares states through F-behaviour after embedding them in T(X), so nondeterministic automata states are equivalent exactly when they recognize the same language.For partial automata, states distinguished by FT-equivalence can still be T-relative equivalent when they accept the same language; ordinary F-behavioural equivalence is contained in the new equivalence.Source: §3 · pp. 7–8

3.1.1. Partial Mealy machines

  • Totalizing a partial Mealy machine with a sink state yields behaviour as a causal function from infinite input streams Aω to output streams Bω.Causality means the nth output depends only on the first n inputs; the sink produces the constant stream of ⊥ outputs.Source: §3.1.1 · p. 8

3.1.2. Structured Moore automata

  • For arbitrary sets A and B and monad T, Moore automata have outputs in T(B) and inputs in A, with final behaviours in T(B)A∗; examples use exception and side-effect monads.For B = 1, these coalgebras coincide with total subsequential transducers.Source: §3.1.2 · pp. 9–10
  • With T the probability-distribution monad and B = 2, the framework captures Rabin probabilistic automata and their probabilistic-language semantics; its equivalences recover probabilistic bisimilarity and trace semantics [19].The paper identifies the semantics with, ordinary ∼F T with probabilistic bisimilarity, and ≈T F with probabilistic transition-system trace semantics [19].Source: §3.1.2 · p. 11

3.2. Pushdown automata, coalgebraically

  • Pushdown machines are modeled using a nondeterministic side-effect monad for stack changes, with transitions constrained to depend on the control state, input, and top stack symbol.A word is accepted exactly when the coalgebraic behaviour evaluates to 1 for the initial control state, word, and stack; the example recognizes {a^n b^n | n ≥ 1}.Source: §3.2 · pp. 12–13

3.2. Pushdown automata, coalgebraically.

  • A Greibach-normal-form grammar yields a coalgebra whose Moore semantics accepts a word exactly when the grammar derives it.The construction sets output to 1 precisely for the empty stack and transitions according to grammar productions.Source: §3.2 · p. 14
  • Two associated Moore automata can accept the same language yet fail behavioural equivalence, differing on abab from stack ss.From ⟨∗, ss⟩, one outputs 1 on abab while the other outputs 0.Source: §3.2 · p. 15
  • This account complements by using Moore automata with outputs in 2^B* and a side-effect monad to characterize context-free languages.The cited account instead uses deterministic automata and the idempotent semiring monad for equivalent presentations via grammars, behavioural differential equations, and generalized regular expressions.Source: §3.2 · pp. 15–16

4. Coalgebras and T-Algebras

Section 4 formalizes structured-state determinization by mapping FT-coalgebras to F-coalgebras over T(X), then relates their behavioural equivalences. It supplies conditions for this lifting and instantiates the resulting implication for familiar automata.

4. Coalgebras and T-Algebras

  • A T-algebra lifting identifies ≈T with ordinary behavioural equivalence for the lifted functor F∗ on T-algebras.For accessible F, the final-coalgebra construction supports this identification.Source: §4 · pp. 16–17
  • A grammar using Id, algebra carriers, products, exponentials, and TG constructs functors with T-algebra liftings; it covers the examples in Sections 2, 3, and 5.The grammar excludes coproducts in general, though the powerset-monad case can be extended with a specified coproduct construction.Source: §4 · p. 16
  • With a final coalgebra and a T-algebra lifting, ∼F T implies ≈T, which is coarser than FT-equivalence.The result is stated for any monad T and endofunctor F satisfying those conditions.Source: §4 · p. 17
  • The construction maps each FT-coalgebra (X, f) to the F-coalgebra (T(X), f♯), and maps FT-homomorphisms through T.The proof uses this mapping as a functor between the coalgebra categories.Source: §4 · p. 17
  • For nondeterministic, partial, and probabilistic automata, the implication specializes to bisimilarity implying language, accepted-word, or probabilistic language equivalence, respectively.The general inclusion can be strict.Source: §4 · p. 18
  • When the monad unit is pointwise injective, FT-equivalence also yields equivalence for the extended TFT-coalgebra, and the lifting result further relates it to ≈T.The stated hierarchy relies on pointwise injectivity for the first implication and a T-algebra lifting for the further relation.Source: §4 · p. 18

5. Beyond Bisimilarity and Traces

Section 5 represents several concurrency equivalences as instances of ≈T, using different functors and state-observation encodings. For LTSs, these include finite trace, complete trace, failure, and ready semantics.

5. Beyond Bisimilarity and Traces

  • Finite trace, complete trace, failure, and ready equivalences for LTSs are characterized as special cases of ≈T.The section takes LTS bisimilarity as the ordinary coalgebraic equivalence from which these examples depart.Source: §5 · p. 19
  • A failure pair records a path word and a set of labels disjoint from enabled labels; a ready pair records the path word and exactly the enabled labels.Complete traces end in a state with no enabled labels.Source: §5 · p. 19
  • In the illustrated systems, all four have the same traces, yet complete-trace, failure, and ready equivalence distinguish some of them.The examples also show that ready equivalence distinguishes every illustrated system.Source: §5 · p. 19
  • For ready semantics, states retain the LTS transitions but are decorated with their enabled-label sets, and the final map records these sets along paths.The map assigns each word the enabled-label sets of states reached by that word.Source: §5 · p. 20
  • Different functors and observation maps encode the other semantics, including failure and trace variants.Failure uses the ready-semantics functor with a new map; trace and complete-trace equivalence use F = 2×idA.Source: §5 · p. 20

6. Discussion

The paper lifts powerset determinization to FT-coalgebras, using monads to structure state spaces across several automata models. It also characterizes pushdown automata and retrieves behavioral equivalences studied in concurrency theory.

6. Discussion

  • The FT-coalgebra framework uniformly treats partial Mealy machines, structured Moore automata, and nondeterministic, partial, and probabilistic automata.The paper also notes that weighted automata [16] fit as structured Moore automata for B = 1 and T = S^ω.Source: §6 · p. 21
  • The framework characterizes pushdown automata and retrieves several behavioral equivalences from concurrency theory.Its weighted-automata example identifies ∼_F T with weighted bisimilarity and ≈_T F with weighted language equivalence.Source: §6 · p. 21
  • Unlike the approach in [19], many examples here fall outside its requirements, and partial Mealy machines are not purely trace-like.The related approach studies TG-coalgebras and G-coalgebras and, under certain assumptions, characterizes generalized trace equivalence.Source: §6 · p. 21
  • The monadic λ-machine approach covers examples such as Moore automata, but not essentially coalgebraic systems such as Mealy machines.A λ-machine has dynamics δ : FX → TX, and induces an implicit λ-machine with TX as its state space.Source: §6 · p. 21
  • Future work includes using F-bisimulations up to T to prove ≈_T F and extending branching-equivalence tools to linear equivalences.The proposed tools include coalgebraic modal logic and axiomatizations for regular expressions.Source: §6 · p. 21
  • A separate paper pursues decorated traces and the full linear-time spectrum, with probabilistic traces planned as a further extension.The authors describe full linear-time-spectrum modeling as challenging.Source: §6 · p. 21
Loading 1302.1046v2…