Handbook of Weighted Automata (eBook)

Preface 5
List of Contributors 9
Contents 11
Part I Foundations 18
Chapter 1: Semirings and Formal Power Series 19
Introduction 19
Monoids and Semirings 21
Formal Power Series 28
Matrices 33
Cycle-Free Linear Equations 38
References 42
Chapter 2: Fixed Point Theory 45
Introduction 45
Some Notation 46
Least Fixed Points 46
Conway Theories 54
Iteration Theories 57
Unique Fixed Points 60
Fixed Points of Linear Functions 62
Inductive *-Semirings 67
Complete Semirings 68
Iterative Semirings 69
Fixed Points of Affine Functions 70
Complete Semiring-Semimodule Pairs 75
Bi-inductive Semiring-Semimodule Pairs 77
References 78
Part II Concepts of Weighted Recognizability 82
Chapter 3: Finite Automata 83
Introduction 83
Finite Automata over Semirings 84
Finite Automata over Arbitrary Power Series Semirings 86
Finite Automata over Conway Semirings 89
Finite Linear Systems 95
Finite Automata over Quemirings 97
Semiring-Semimodule Pairs and Quemirings 99
Finite Automata over Quemirings and a Kleene Theorem 105
Finite Linear Systems over Quemirings 113
References 117
Chapter 4: Rational and Recognisable Power Series 119
Introduction 120
Rational Series and Weighted Rational Expressions 121
Series over a Graded Monoid 121
Graded Monoid 123
Topology on S< <
Distance on S< <
Summable Families 126
Rational Series 128
Star of a Series 128
Star of a Proper Series 129
Strong Semirings and Star of an Arbitrary Series 130
The Family of Rational Series 132
S-Rational Operations 132
Characteristic Series and Unambiguous Rational Sets 133
Rational S-Expressions 134
Weighted Automata 136
The Behaviour of a Weighted Automaton 136
The Fundamental Theorem of Automata 140
Proper Automata 141
Standard Automata 142
Statement and Proof of the Fundamental Theorem 144
Conjugacy and Covering of Automata 146
From Conjugacy to Covering 146
Minimal S-Quotient 148
From Covering to Conjugacy 150
Recognisable Series and Representations 152
The Family of Recognisable Series 152
Other Products on Recognisable Series 155
Tensor Product of S-Representations 155
Hadamard Product 156
Shuffle Product 157
Series on a Product of Monoids 159
The Canonical Isomorphisms 159
Rational Series in a Product 160
Weighted Relations 161
Morphic Image of Recognisable and Rational Series 163
Series over a Free Monoid 165
The Representability Theorem 166
Characterisation of Recognisable Series 166
Derivation of Rational S-Expressions 168
S-Derivatives 168
The Derived Term Automaton 169
Reduced Representations 171
Rank of a Series 171
The Reduction Algorithm 172
Word Base 172
Demonstration of the Reduction Theorem (Theorem 5.20) 174
Applications of the Reduction of Representations 175
Equivalence Decidability 176
Recurrence Relations 177
From Equivalence to Conjugacy 178
Support of Rational Series 179
Notes 182
General Sources 182
Notes to Sect. 2: Rational Series 183
Notes to Sect. 3: Weighted Automata 183
Notes to Sect. 4: Recognisable Series 184
Notes to Sect. 5: Series over a Free Monoid 184
Notes to Sect. 6: Support of Rational Series 185
References 185
Chapter 5: Weighted Automata and Weighted Logics 189
Introduction 189
MSO-Logic and Weighted Automata 192
Weighted Logics 195
Unambiguous Formulas 199
Definability Equals Recognizability 203
Locally Finite Semirings 208
Weighted Automata on Infinite Words 211
Weighted Logics on Infinite Words 217
Conclusions and Open Problems 220
Open problems: 221
References 222
Chapter 6: Weighted Automata Algorithms 226
Introduction 227
Preliminaries 227
Semirings 227
Weighted Transducers and Automata 228
Shortest-Distance Algorithms 230
All-Pairs Shortest-Distance Problems 231
Complete Semirings 231
All-Pairs Shortest-Distance Algorithm 232
Single-Source Shortest-Distance Problems 235
k-Closed Semirings 235
General Single-Source Shortest-Distance Algorithm 235
Rational Operations 236
Elementary Unary Operations 239
Fundamental Binary Operations 239
Composition 239
Intersection 244
Difference 244
Optimization Algorithms 246
Epsilon-Removal 246
Determinization 250
Weight Pushing 254
Minimization 256
Synchronization 259
Conclusion 263
References 263
Part III Weighted Discrete Structures 268
Chapter 7: Algebraic Systems and Pushdown Automata 269
Introduction 269
Auxiliary Notions and Results 270
Algebraic Power Series 273
Definition and Basic Reductions 273
Interconnections with Context-Free Grammars 277
Normal Forms 279
Theorems of Shamir and Chomsky-Schützenberger 283
Transductions 287
Pushdown Automata 291
Pushdown Transition Matrices 291
S< <
Equivalence with Algebraic Systems 296
Other Topics 299
References 300
Chapter 8: Lindenmayer Systems 302
Introduction 302
Iterated Morphisms and Rational Series 303
Lindenmayerian Algebraic Series 307
D0L Power Series 313
Other Power Series Generalizations of L Systems 318
References 320
Chapter 9: Weighted Tree Automata and Tree Transducers 323
Introduction 324
Preliminaries 326
General Notation 326
Trees 326
Algebraic Concepts 327
Tree Series 330
Weighted Tree Automata 330
Bottom-up Tree Automata 330
Recognizable Tree Series 331
Closure Properties 336
Support of Recognizable Tree Series 338
Determinization of Weighted Tree Automata 340
Pumping Lemmata and Decidability 341
Finite Algebraic Characterizations of Recognizable Tree Series 345
Characterizations for Fields 346
Characterizations for Semifields 348
Characterizations for Commutative, Zero-Divisor Free Semirings 352
Equational Tree Series 352
Solutions over the S-Sigma-Semimodule of Tree Series 353
Solutions over Arbitrary S-Sigma-Semimodules 356
Rational Tree Series 357
MSO-Definable Tree Series 359
Other Models Related to Recognizable Tree Series 363
S-Sigma-Tree Automata 363
Finite, Polynomial Tree Automata 363
Multilinear Representations 365
S-Sigma-Representations 366
Polynomially-Weighted Tree Automata 370
Wta over Distributive Multioperator Monoids 370
Further Results 370
IO-Substitution and Tree Series Transformations 371
Weighted Tree Transducers 374
Tree Transducers 374
The Basic Model 375
Restricted Models 380
Composition and Decomposition 384
Results Concerning wtt 385
Results Concerning Bottom-up wtt 388
Results Concerning Top-down wtt 392
The Inclusion Diagram of Some Fundamental wtt Classes 396
Hierarchies 398
Further Models of Weighted Tree Transducers 401
Bottom-up Inf-wtt with OI-Substitution 401
Inf-wtt with OI-Substitution 402
Top-down Inf-wtt and Bottom-up Inf-wtt with IOo-Substitution 402
Top-down and Bottom-up Inf-wtt with Term Rewrite Semantics 403
Deterministic Bottom-up Inf-wtt over Multiplicative Monoids 403
Further Results 404
References 404
Chapter 10: Traces, Series-Parallel Posets, and Pictures: A Weighted Study 414
Introduction 415
Traces 416
Weighted Distributed Systems 416
Weighted Asynchronous Cellular Automata 417
Word Behavior of wACA 417
Interleaving Behavior of wACA 418
Concurrent Behavior of wACA 418
Relations Between These Behaviors 419
Other Formalisms: Presentations, Expressions, and Logics 420
Presentations 420
Expressions 420
Logic 421
Relating the Formalisms 422
Property (T) 422
wACA, (Word Series) Presentations, and Property (T) 423
From wACA to Presentations 423
From Presentations to Word Series Presentations 423
From Word Series Presentations to Property (Tlex) 424
From Property (T) to wACA 425
wACA, Logic, and Word Series Presentations 425
A Fragment of Weighted Monadic Second-Order Logic 425
From wACA to Logic 426
From Logic to Word Series Presentations 427
Expressions and Property (T) 428
From Property (Tlex) to Expressions 428
From Expressions to Property (T) 428
The Characterization Theorem 429
History and Overview 430
Series-Parallel Posets 432
Series-Parallel Posets and Bisemirings 432
Series-Parallel Posets 432
Bisemirings 433
Weighted Branching Automata 434
Rationality 436
Rational Expressions 437
From Rational Expressions to Weighted Branching Automata 437
From Weighted Branching Automata to Expressions 440
Bounded Depth and Bounded Width 441
The Characterization Theorem 442
The Hadamard Product 442
History and Overview 444
Pictures 445
Pictures and Weighted Picture Automata 445
Weighted 2-Dimensional On-line Tessellation Automata 446
Weighted Tiling Systems 447
Other Formalisms: Expressions and Logics 447
Rational Picture Series 447
Logic 448
Relating the Formalisms 449
Recognizable and Rational Picture Series 449
Recognizable Picture Series and Logics 450
The Characterization Theorem 453
Decidability Issues 453
History and Overview 454
References 455
Part IV Applications 460
Chapter 11: Digital Image Compression 461
Introduction 461
Image Types 462
Weighted Finite Automata and Multi-resolution Images 465
Drawing WFA Images 467
Decoding Algorithm #1 468
Decoding Algorithm #2 468
An Encoding Algorithm 468
Encoding Algorithm for Grayscale Images 469
Practical Image Compression Using WFA 471
Encoding Algorithm #2 472
Weighted Finite Transducers (WFT) 477
Parametric Weighted Finite Automata (PWFA) 480
PWFA over Unary Alphabet 482
PWFA and Iterated Function Systems 483
PWFA and Polynomial Curves 483
Conclusions and Open Problems 484
References 485
Chapter 12: Fuzzy Languages 488
Introduction 488
Lattices and Fuzzy Languages 490
Fuzzy Recognizability over Bounded Distributive Lattices 493
Fuzzy Recognizability over Finite Words 494
Fuzzy Recognizability over Infinite Words 502
Multi-valued MSO Logic 507
Fuzzy Languages: An Overview 512
Fuzzy Languages over l-Monoids 513
Fuzzy Languages over Residuated Lattices 514
Fuzzy Automata with Outputs 516
Fuzzy Abstract Families of Languages 516
Fuzzy Tree Languages 516
Applications 517
References 520
Chapter 13: Model Checking Linear-Time Properties of Probabilistic Systems 525
Introduction 525
About This Chapter 531
Markov Decision Processes 532
Paths and Schedulers of an MDP 534
Specifying Systems with an MDP-Semantics 536
Maximal Reachability Probabilities 539
Implementation Issues 542
Model Checking omega-Regular Properties 544
Computing the Set of Maximal end Components 550
Case 1: A Is a Deterministic Rabin Automaton 551
Case 2: A Is a Deterministic Streett Automaton 551
Calculating the Set AMEC 552
Partial Order Reduction 553
The Ample Set Method for MDPs and LT Properties 555
Experimental Results 562
Partially Observable MDPs 563
Conclusion 565
Appendix 566
Markov Chains 566
Markov Decision Processes 568
References 569
Chapter 14: Applications of Weighted Automata in Natural Language Processing 577
Background 577
WFST Techniques for Natural Language Processing 578
Example 1: Transliteration 579
Example 2: Translation 584
Language Modeling 588
Applications of Weighted String Automata 589
Language Translation 590
Speech Recognition 590
Lexical Processing 591
Tagging 591
Summarization 592
Optical Character Recognition 592
Applications of Weighted Tree Automata 592
Open Problems 596
Conclusion 597
References 597
Index 603