-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathreferences.bib
1582 lines (1378 loc) · 131 KB
/
references.bib
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
%% This BibTeX bibliography file was created using BibDesk.
%% http://bibdesk.sourceforge.net/
%% Created for Florent Jacquemard at 2021-10-15 13:33:08 +0200
%% Saved with string encoding Unicode (UTF-8)
@inproceedings{Kwiatkowska07quantitativeVerif,
author = {Kwiatkowska, Marta},
booktitle = {Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering},
date-added = {2021-10-15 10:19:52 +0200},
date-modified = {2021-10-15 10:20:05 +0200},
pages = {449--458},
title = {Quantitative verification: models techniques and tools},
year = {2007}}
@phdthesis{:aa,
date-added = {2021-10-15 10:19:33 +0200},
date-modified = {2021-10-15 10:19:33 +0200}}
@inproceedings{Mathissen08weighted,
author = {Mathissen, Christian},
booktitle = {International Colloquium on Automata, Languages, and Programming},
date-added = {2021-10-13 22:18:05 +0200},
date-modified = {2021-10-13 22:18:05 +0200},
organization = {Springer},
pages = {221--232},
title = {Weighted logics for nested words and algebraic formal power series},
year = {2008},
bdsk-file-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxBdLi4vLi4vLi4vTGlicmFyeS9Nb2JpbGUgRG9jdW1lbnRzL2NvbX5hcHBsZX5DbG91ZERvY3MvQmlibGlvL0FydGljbGVzL01hdGhpc3NlbjA4d2VpZ2h0ZWQucGRmTxEBzAAAAAABzAACAAAHc3lzdGVtZQAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAEJEAAH/////F01hdGhpc3NlbjA4d2VpZ2h0ZWQucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAP////8AAAAAAAAAAAAAAAAAAwAGAAAKIGN1AAAAAAAAAAAAAAAAAAhBcnRpY2xlcwACAGUvOlVzZXJzOmphY3F1ZW1hOkxpYnJhcnk6TW9iaWxlIERvY3VtZW50czpjb21+YXBwbGV+Q2xvdWREb2NzOkJpYmxpbzpBcnRpY2xlczpNYXRoaXNzZW4wOHdlaWdodGVkLnBkZgAADgAwABcATQBhAHQAaABpAHMAcwBlAG4AMAA4AHcAZQBpAGcAaAB0AGUAZAAuAHAAZABmAA8AEAAHAHMAeQBzAHQAZQBtAGUAEgBjVXNlcnMvamFjcXVlbWEvTGlicmFyeS9Nb2JpbGUgRG9jdW1lbnRzL2NvbX5hcHBsZX5DbG91ZERvY3MvQmlibGlvL0FydGljbGVzL01hdGhpc3NlbjA4d2VpZ2h0ZWQucGRmAAATAAEvAAAVAAIAD///AAAACAANABoAJACEAAAAAAAAAgEAAAAAAAAABQAAAAAAAAAAAAAAAAAAAlQ=}}
@inproceedings{VeanesBBjorner12SAtoolkit,
author = {Veanes, Margus and Bj{\o}rner, Nikolaj},
booktitle = {International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
date-added = {2021-10-13 16:44:11 +0200},
date-modified = {2021-10-13 16:44:42 +0200},
organization = {Springer},
pages = {472--477},
title = {Symbolic automata: The toolkit},
year = {2012}}
@article{BarHillel61formai,
author = {Bar-Hillel, Yehoshua and Perles, Micha and Shamir, Eli},
date-added = {2021-10-13 16:39:28 +0200},
date-modified = {2021-10-13 16:39:59 +0200},
journal = {STUF-Language Typology and Universals},
number = {1-4},
pages = {143--172},
publisher = {AKADEMIE VERLAG},
title = {On formai properties of simple phrase structure grammars},
volume = {14},
year = {1961}}
@inproceedings{NederhofSatta03ParsingIntersection,
author = {Nederhof, Mark-Jan and Satta, Giorgio},
booktitle = {Proceedings of the Eighth International Conference on Parsing Technologies},
date-added = {2021-09-02 09:06:56 +0200},
date-modified = {2021-09-02 09:38:24 +0200},
pages = {137--148},
title = {Probabilistic parsing as intersection},
year = {2003}}
@phdthesis{Herrmann20phd,
abstract = {In this thesis, we investigate weighted tree automata with storage theoretically.
This model generalises finite state automata in three dimensions:
(i) from words to trees,
(ii) by using an arbitrary storage type in addition to a finite-state control, and
(iii) by considering languages in a quantitative setting using a weight structure.
},
address = {Dresden},
annote = {supervisor Prof. Dr. Heiko Vogler
},
author = {Herrmann, Luisa},
date-added = {2021-09-01 14:27:20 +0200},
date-modified = {2021-09-01 14:27:20 +0200},
keywords = {weighted automata with storage, weighted tree automata, multioperator monoids},
school = {Technische Universit{\"a}t Dresden},
title = {Weighted Automata with Storage},
year = {2020},
bdsk-file-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxBVLi4vLi4vLi4vTGlicmFyeS9Nb2JpbGUgRG9jdW1lbnRzL2NvbX5hcHBsZX5DbG91ZERvY3MvQmlibGlvL1RoZXNlcy9IZXJybWFubjIwcGhkLnBkZk8RAa4AAAAAAa4AAgAAB3N5c3RlbWUAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAABCRAAB/////xFIZXJybWFubjIwcGhkLnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAD/////AAAAAAAAAAAAAAAAAAMABgAACiBjdQAAAAAAAAAAAAAAAAAGVGhlc2VzAAIAXS86VXNlcnM6amFjcXVlbWE6TGlicmFyeTpNb2JpbGUgRG9jdW1lbnRzOmNvbX5hcHBsZX5DbG91ZERvY3M6QmlibGlvOlRoZXNlczpIZXJybWFubjIwcGhkLnBkZgAADgAkABEASABlAHIAcgBtAGEAbgBuADIAMABwAGgAZAAuAHAAZABmAA8AEAAHAHMAeQBzAHQAZQBtAGUAEgBbVXNlcnMvamFjcXVlbWEvTGlicmFyeS9Nb2JpbGUgRG9jdW1lbnRzL2NvbX5hcHBsZX5DbG91ZERvY3MvQmlibGlvL1RoZXNlcy9IZXJybWFubjIwcGhkLnBkZgAAEwABLwAAFQACAA///wAAAAgADQAaACQAfAAAAAAAAAIBAAAAAAAAAAUAAAAAAAAAAAAAAAAAAAIu},
bdsk-url-1 = {https://nbn-resolving.org/urn:nbn:de:bsz:14-qucosa2-740685}}
@inproceedings{Herrmann16dlt,
author = {Herrmann, Luisa and Vogler, Heiko},
booktitle = {International Conference on Developments in Language Theory},
date-added = {2021-09-01 14:23:18 +0200},
date-modified = {2021-09-01 14:23:47 +0200},
keywords = {VPA, Weighted Automata},
organization = {Springer},
pages = {203--215},
title = {Weighted Symbolic Automata with Data Storage},
year = {2016},
bdsk-file-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxBbLi4vLi4vLi4vTGlicmFyeS9Nb2JpbGUgRG9jdW1lbnRzL2NvbX5hcHBsZX5DbG91ZERvY3MvQmlibGlvL1NsaWRlcy9IZXJtYW5uMTZkbHRfc2xpZGVzLnBkZk8RAcYAAAAAAcYAAgAAB3N5c3RlbWUAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAABCRAAB/////xdIZXJtYW5uMTZkbHRfc2xpZGVzLnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAD/////AAAAAAAAAAAAAAAAAAMABgAACiBjdQAAAAAAAAAAAAAAAAAGU2xpZGVzAAIAYy86VXNlcnM6amFjcXVlbWE6TGlicmFyeTpNb2JpbGUgRG9jdW1lbnRzOmNvbX5hcHBsZX5DbG91ZERvY3M6QmlibGlvOlNsaWRlczpIZXJtYW5uMTZkbHRfc2xpZGVzLnBkZgAADgAwABcASABlAHIAbQBhAG4AbgAxADYAZABsAHQAXwBzAGwAaQBkAGUAcwAuAHAAZABmAA8AEAAHAHMAeQBzAHQAZQBtAGUAEgBhVXNlcnMvamFjcXVlbWEvTGlicmFyeS9Nb2JpbGUgRG9jdW1lbnRzL2NvbX5hcHBsZX5DbG91ZERvY3MvQmlibGlvL1NsaWRlcy9IZXJtYW5uMTZkbHRfc2xpZGVzLnBkZgAAEwABLwAAFQACAA///wAAAAgADQAaACQAggAAAAAAAAIBAAAAAAAAAAUAAAAAAAAAAAAAAAAAAAJM}}
@article{Knuth77,
author = {Knuth, Donald},
date-added = {2021-09-01 14:23:07 +0200},
date-modified = {2021-10-12 11:22:50 +0200},
journal = {Inform. Process. Lett.},
number = {1},
title = {A generalization of {D}ijkstra's algorithm},
volume = {6},
year = {1977}}
@incollection{NederhofSatta04tabular,
author = {Nederhof, Mark-Jan and Satta, Giorgio},
booktitle = {Formal Languages and Applications},
date-added = {2021-09-01 14:22:49 +0200},
date-modified = {2021-09-01 14:22:49 +0200},
pages = {529--549},
publisher = {Springer},
title = {Tabular Parsing},
year = {2004},
bdsk-file-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxBgLi4vLi4vLi4vTGlicmFyeS9Nb2JpbGUgRG9jdW1lbnRzL2NvbX5hcHBsZX5DbG91ZERvY3MvQmlibGlvL0FydGljbGVzL05lZGVyaG9mU2F0dGEwNHRhYnVsYXIucGRmTxEB1gAAAAAB1gACAAAHc3lzdGVtZQAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAEJEAAH/////Gk5lZGVyaG9mU2F0dGEwNHRhYnVsYXIucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAP////8AAAAAAAAAAAAAAAAAAwAGAAAKIGN1AAAAAAAAAAAAAAAAAAhBcnRpY2xlcwACAGgvOlVzZXJzOmphY3F1ZW1hOkxpYnJhcnk6TW9iaWxlIERvY3VtZW50czpjb21+YXBwbGV+Q2xvdWREb2NzOkJpYmxpbzpBcnRpY2xlczpOZWRlcmhvZlNhdHRhMDR0YWJ1bGFyLnBkZgAOADYAGgBOAGUAZABlAHIAaABvAGYAUwBhAHQAdABhADAANAB0AGEAYgB1AGwAYQByAC4AcABkAGYADwAQAAcAcwB5AHMAdABlAG0AZQASAGZVc2Vycy9qYWNxdWVtYS9MaWJyYXJ5L01vYmlsZSBEb2N1bWVudHMvY29tfmFwcGxlfkNsb3VkRG9jcy9CaWJsaW8vQXJ0aWNsZXMvTmVkZXJob2ZTYXR0YTA0dGFidWxhci5wZGYAEwABLwAAFQACAA///wAAAAgADQAaACQAhwAAAAAAAAIBAAAAAAAAAAUAAAAAAAAAAAAAAAAAAAJh}}
@incollection{NederhofSatta08probabilisticparsing,
author = {Nederhof, Mark-Jan and Satta, Giorgio},
booktitle = {New Developments in Formal Languages and Applications},
date-added = {2021-09-01 14:22:49 +0200},
date-modified = {2021-09-01 14:22:49 +0200},
pages = {229--258},
publisher = {Springer},
title = {Probabilistic Parsing},
year = {2008},
bdsk-file-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxBhLi4vLi4vLi4vTGlicmFyeS9Nb2JpbGUgRG9jdW1lbnRzL2NvbX5hcHBsZX5DbG91ZERvY3MvQmlibGlvL0FydGljbGVzL05lZGVyaG9mU2F0dGEwOHBwYXJzaW5nLnBkZk8RAdwAAAAAAdwAAgAAB3N5c3RlbWUAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAABCRAAB/////xtOZWRlcmhvZlNhdHRhMDhwcGFyc2luZy5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAD/////AAAAAAAAAAAAAAAAAAMABgAACiBjdQAAAAAAAAAAAAAAAAAIQXJ0aWNsZXMAAgBpLzpVc2VyczpqYWNxdWVtYTpMaWJyYXJ5Ok1vYmlsZSBEb2N1bWVudHM6Y29tfmFwcGxlfkNsb3VkRG9jczpCaWJsaW86QXJ0aWNsZXM6TmVkZXJob2ZTYXR0YTA4cHBhcnNpbmcucGRmAAAOADgAGwBOAGUAZABlAHIAaABvAGYAUwBhAHQAdABhADAAOABwAHAAYQByAHMAaQBuAGcALgBwAGQAZgAPABAABwBzAHkAcwB0AGUAbQBlABIAZ1VzZXJzL2phY3F1ZW1hL0xpYnJhcnkvTW9iaWxlIERvY3VtZW50cy9jb21+YXBwbGV+Q2xvdWREb2NzL0JpYmxpby9BcnRpY2xlcy9OZWRlcmhvZlNhdHRhMDhwcGFyc2luZy5wZGYAABMAAS8AABUAAgAP//8AAAAIAA0AGgAkAIgAAAAAAAACAQAAAAAAAAAFAAAAAAAAAAAAAAAAAAACaA==}}
@electronic{qparse,
date-added = {2021-07-19 22:41:10 +0200},
date-modified = {2021-07-19 22:42:28 +0200},
title = {qparse, a library for automated rhythm transcription},
url = {https://qparse.gitlabpages.inria.fr},
bdsk-url-1 = {https://qparse.gitlabpages.inria.fr}}
@book{Selfridge-Field97beyondMIDI,
annote = {author: Byrd, Donald and Boyle, Roger D and Berggren, Ulf and Bainbridge, David and others},
date-added = {2021-07-12 14:44:37 +0200},
date-modified = {2021-07-12 14:50:40 +0200},
editor = {Eleanor Selfridge-Field},
publisher = {MIT press},
title = {Beyond MIDI: the handbook of musical codes},
url = {http://beyondmidi.ccarh.org/beyondmidi-600dpi.pdf},
year = {1997},
bdsk-url-1 = {http://beyondmidi.ccarh.org/beyondmidi-600dpi.pdf}}
@article{Bahar97ADD,
annote = {
**Algebraic Decision Diagrams** (ADDs)
> R Iris Bahar, Erica A Frohm, Charles M Gaona, Gary D Hachtel, Enrico Macii, Abelardo Pardo, and Fabio Somenzi
> Algebric decision diagrams and their applications
> Formal methods in system design 10, 2-3 (1997), 171--206. 1997.
https://link.springer.com/content/pdf/10.1023/A:1008699807402.pdf
via [Inria](http://sfx-33pup.hosted.exlibrisgroup.com/33inria?sid=google&auinit=RI&aulast=Bahar&atitle=Algebric+decision+diagrams+and+their+applications&id=doi:10.1023/A:1008699807402&title=Formal+Methods+in+System+Design&volume=10&issue=2-3&date=1997&spage=171&issn=0925-9856)
= generalization of **Binary Decision Diagrams** (BDDs)
> Bryant
> Graph-Based Algorithms for Boolean Function Manipulation
> IEEE Trans. Comput. C-35, 8 (1986), 677--691. 1986.
---
**definition**
= representation a transition functions/relations
= 4-tuple: $(X, T, \pi, G)$ where
- $X$ : Boolean variable set
- $T$ : finite *carrier* set:
- $\{ 0, 1\}$ for BDD,
- subset of $\R$ for ADD.
- $\pi$: $X \to \N$ (diagram variable order)
- $G$: rooted DAG such that
- every terminal node labeled with element of $T$
- every non-terminal node labeled with element of $X$
and has two outgoing edges labeled $0$ and $1$
- for every path in $G$ , labels of visited non-terminal nodes occur in increasing order *wrt* $\pi$
= representation as DAG of a Boolean function of the form:
- $2^X \to \{ 0, 1\}$ for BDD
- $2^X \to \R$ for ADD
---
**properties**
operations on Boolean fucntions computable in PTIME on the BDD repr. :
- conjunction
- disjunction
- if-then-else
- existential quantification
operations on Boolean fucntions computable in PTIME on the ADD repr. :
- product
- sum
- if-then-else
- additive quatification
- variable abstraction (reduce dimensionality)
- `Apply`
- `Abstract`
---
**applications** (ADD)
**matrix multiplication** in nsemirinngs and quasi-rings
representation of matrices by ADDs
algorithm based on recursive application of Boole's expansion theorem.
**shortest path algos**
implantation efficient for large graphs
(> $10^{27}$ vertices and $10^{36}$ nodes):
[single source algos]
- Dijkstra
- Bellman-Ford
[all-pairs algos]
- Repeated-Squaring
- Floyd-Marshall
- Johnson
**solution of systems of linear equations**
implantation of Gaussian elimination followed by back substitution.
},
author = {Bahar, R Iris and Frohm, Erica A and Gaona, Charles M and Hachtel, Gary D and Macii, Enrico and Pardo, Abelardo and Somenzi, Fabio},
date-added = {2021-07-06 14:38:44 +0200},
date-modified = {2021-07-07 21:52:19 +0200},
journal = {Formal methods in system design},
number = {2-3},
pages = {171--206},
publisher = {Springer},
title = {Algebraic Decision Diagrams and their Applications},
volume = {10},
year = {1997},
bdsk-file-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxBULi4vLi4vLi4vTGlicmFyeS9Nb2JpbGUgRG9jdW1lbnRzL2NvbX5hcHBsZX5DbG91ZERvY3MvQmlibGlvL0FydGljbGVzL0JhaGFyOTdBREQucGRmTxEBpgAAAAABpgACAAAHc3lzdGVtZQAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAEJEAAH/////DkJhaGFyOTdBREQucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAP////8AAAAAAAAAAAAAAAAAAwAGAAAKIGN1AAAAAAAAAAAAAAAAAAhBcnRpY2xlcwACAFwvOlVzZXJzOmphY3F1ZW1hOkxpYnJhcnk6TW9iaWxlIERvY3VtZW50czpjb21+YXBwbGV+Q2xvdWREb2NzOkJpYmxpbzpBcnRpY2xlczpCYWhhcjk3QURELnBkZgAOAB4ADgBCAGEAaABhAHIAOQA3AEEARABEAC4AcABkAGYADwAQAAcAcwB5AHMAdABlAG0AZQASAFpVc2Vycy9qYWNxdWVtYS9MaWJyYXJ5L01vYmlsZSBEb2N1bWVudHMvY29tfmFwcGxlfkNsb3VkRG9jcy9CaWJsaW8vQXJ0aWNsZXMvQmFoYXI5N0FERC5wZGYAEwABLwAAFQACAA///wAAAAgADQAaACQAewAAAAAAAAIBAAAAAAAAAAUAAAAAAAAAAAAAAAAAAAIl}}
@inproceedings{LombardySakarovitch12ciaa,
abstract = {The removal of ε-transitions in weighted automata leads to infinite summation when cycles of such transitions are allowed.
This paper presents both an algorithm for that purpose, and a framework in which the algorithm is correct.},
author = {Lombardy, Sylvain and Sakarovitch, Jacques},
booktitle = {International Conference on Implementation and Application of Automata},
date-added = {2021-06-01 14:58:25 +0200},
date-modified = {2021-06-01 14:58:25 +0200},
keywords = {weighted automata},
organization = {Springer},
pages = {345--352},
title = {The removal of weighted $\varepsilon$-transitions},
year = {2012},
bdsk-file-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxBjLi4vLi4vLi4vTGlicmFyeS9Nb2JpbGUgRG9jdW1lbnRzL2NvbX5hcHBsZX5DbG91ZERvY3MvQmlibGlvL0FydGljbGVzL0xvbWJhcmR5U2FrYXJvdml0Y2gxMmNpYWEucGRmTxEB5AAAAAAB5AACAAAHc3lzdGVtZQAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAEJEAAH/////HUxvbWJhcmR5U2FrYXJvdml0Y2gxMmNpYWEucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAP////8AAAAAAAAAAAAAAAAAAwAGAAAKIGN1AAAAAAAAAAAAAAAAAAhBcnRpY2xlcwACAGsvOlVzZXJzOmphY3F1ZW1hOkxpYnJhcnk6TW9iaWxlIERvY3VtZW50czpjb21+YXBwbGV+Q2xvdWREb2NzOkJpYmxpbzpBcnRpY2xlczpMb21iYXJkeVNha2Fyb3ZpdGNoMTJjaWFhLnBkZgAADgA8AB0ATABvAG0AYgBhAHIAZAB5AFMAYQBrAGEAcgBvAHYAaQB0AGMAaAAxADIAYwBpAGEAYQAuAHAAZABmAA8AEAAHAHMAeQBzAHQAZQBtAGUAEgBpVXNlcnMvamFjcXVlbWEvTGlicmFyeS9Nb2JpbGUgRG9jdW1lbnRzL2NvbX5hcHBsZX5DbG91ZERvY3MvQmlibGlvL0FydGljbGVzL0xvbWJhcmR5U2FrYXJvdml0Y2gxMmNpYWEucGRmAAATAAEvAAAVAAIAD///AAAACAANABoAJACKAAAAAAAAAgEAAAAAAAAABQAAAAAAAAAAAAAAAAAAAnI=}}
@book{Gould11Notation,
annote = {Contents
I. GENERAL CONVENTIONS
1. Ground Rules
2. Chords - Dotted notes - Ties
3. Accidentals and Key Signatures
4. Dynamics and Articulation
5. Grace Notes, Arpeggiated Chords, Trills, Glissandos and Vibrato
6. Metre
7. Tuplets
8. Repeat Signs
II. IDIOMATIC NOTATION
9. Woodwind and Brass
10. Percussion
11. Keyboard
12. Harp
13. Classical Guitar
14. Strings
15. Vocal Music
II. LAYOUT AND PRESENTATION
16. Preparing Materials
17. Score Layout
18. Part Preparation
19. Electroacoustic Music
20. Freedom and Choice},
author = {Elaine Gould},
date-added = {2021-06-01 10:45:25 +0200},
date-modified = {2021-06-01 10:45:25 +0200},
publisher = {Faber Music},
title = {Behind Bars: The Definitive Guide to Music Notation},
year = {2011}}
@inproceedings{Bjorklund15best,
author = {Bj{\"o}rklund, Johanna and Drewes, Frank and Zechner, Niklas},
booktitle = {Proc. 9th International Conference on Language and Automata Theory and Applications (LATA)},
date-added = {2021-05-25 10:52:31 +0200},
date-modified = {2021-05-25 10:52:31 +0200},
institution = {Ume{\aa} University, Department of Computing Science},
number = {8977},
pages = {97--108},
series = {Lecture Notes in Computer Science},
title = {An efficient best-trees algorithm for weighted tree automata over the tropical semiring},
year = {2015},
bdsk-file-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxBZLi4vLi4vLi4vTGlicmFyeS9Nb2JpbGUgRG9jdW1lbnRzL2NvbX5hcHBsZX5DbG91ZERvY3MvQmlibGlvL0FydGljbGVzL0Jqb3JrbHVuZDE1YmVzdC5wZGZPEQG8AAAAAAG8AAIAAAdzeXN0ZW1lAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAQkQAAf////8TQmpvcmtsdW5kMTViZXN0LnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA/////wAAAAAAAAAAAAAAAAADAAYAAAogY3UAAAAAAAAAAAAAAAAACEFydGljbGVzAAIAYS86VXNlcnM6amFjcXVlbWE6TGlicmFyeTpNb2JpbGUgRG9jdW1lbnRzOmNvbX5hcHBsZX5DbG91ZERvY3M6QmlibGlvOkFydGljbGVzOkJqb3JrbHVuZDE1YmVzdC5wZGYAAA4AKAATAEIAagBvAHIAawBsAHUAbgBkADEANQBiAGUAcwB0AC4AcABkAGYADwAQAAcAcwB5AHMAdABlAG0AZQASAF9Vc2Vycy9qYWNxdWVtYS9MaWJyYXJ5L01vYmlsZSBEb2N1bWVudHMvY29tfmFwcGxlfkNsb3VkRG9jcy9CaWJsaW8vQXJ0aWNsZXMvQmpvcmtsdW5kMTViZXN0LnBkZgAAEwABLwAAFQACAA///wAAAAgADQAaACQAgAAAAAAAAAIBAAAAAAAAAAUAAAAAAAAAAAAAAAAAAAJA}}
@article{Jonsson17nbest,
abstract = {We propose an algorithm for computing the N best vertices in a weighted acyclic hypergraph over a nice semiring. A semiring is nice if it is finitely-generated, idempotent, and has 1 as its minimal element.
We then apply the algorithm to the problem of computing the N best trees with respect to a weighted tree automaton, and complement theoretical correctness and complexity arguments with experimental data. The algorithm has several practical applications in natural language processing, for example, to derive the N most likely parse trees with respect to a probabilistic context-free grammar.},
author = {Bj{\"o}rklund, Johanna and Drewes, Frank and Jonsson, Anna},
date-added = {2021-05-25 10:52:10 +0200},
date-modified = {2021-05-25 10:52:10 +0200},
doi = {https://doi.org/10.1016/j.tcs.2017.03.010},
journal = {Theoretical Computer Science},
keywords = {Hypergraph, N-best problem, Idempotent semiring},
pages = {30-41},
title = {Finding the N best vertices in an infinite weighted hypergraph},
volume = {682},
year = {2017},
bdsk-file-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxBYLi4vLi4vLi4vTGlicmFyeS9Nb2JpbGUgRG9jdW1lbnRzL2NvbX5hcHBsZX5DbG91ZERvY3MvQmlibGlvL0FydGljbGVzL0pvbnNzb24xN25iZXN0LnBkZk8RAbYAAAAAAbYAAgAAB3N5c3RlbWUAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAABCRAAB/////xJKb25zc29uMTduYmVzdC5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAD/////AAAAAAAAAAAAAAAAAAMABgAACiBjdQAAAAAAAAAAAAAAAAAIQXJ0aWNsZXMAAgBgLzpVc2VyczpqYWNxdWVtYTpMaWJyYXJ5Ok1vYmlsZSBEb2N1bWVudHM6Y29tfmFwcGxlfkNsb3VkRG9jczpCaWJsaW86QXJ0aWNsZXM6Sm9uc3NvbjE3bmJlc3QucGRmAA4AJgASAEoAbwBuAHMAcwBvAG4AMQA3AG4AYgBlAHMAdAAuAHAAZABmAA8AEAAHAHMAeQBzAHQAZQBtAGUAEgBeVXNlcnMvamFjcXVlbWEvTGlicmFyeS9Nb2JpbGUgRG9jdW1lbnRzL2NvbX5hcHBsZX5DbG91ZERvY3MvQmlibGlvL0FydGljbGVzL0pvbnNzb24xN25iZXN0LnBkZgATAAEvAAAVAAIAD///AAAACAANABoAJAB/AAAAAAAAAgEAAAAAAAAABQAAAAAAAAAAAAAAAAAAAjk=},
bdsk-url-1 = {https://doi.org/10.1016/j.tcs.2017.03.010}}
@article{FulopVogler19acta,
abstract = {We combine three extensions of context-free grammars:
(a) associating its nonterminals with storage configurations,
(b) equipping its rules with weights, and
(c) controlling its derivations.
For a commutative semiring K , we introduce the class of weighted languages generated by K-weighted linear context-free grammars with storage S and with derivations controlled by (S, K)-recognizable weighted languages. The control on the derivations can be iterated in a natural way. We characterize the n-th iteration of the control in terms of the n-th iteration of the one-turn pushdown operator on the storage S of the control weighted language. Moreover, for each proper semiring we prove that iterating the control yields an infinite, strict hierarchy of classes of weighted languages.
},
author = {F{\"u}l{\"o}p, Zolt{\'a}n and Vogler, Heiko},
date-added = {2021-05-13 14:45:54 +0200},
date-modified = {2021-05-13 14:49:18 +0200},
doi = {https://doi.org/10.1007/s00236-018-0325-x},
journal = {Acta Informatica},
number = {5},
pages = {447--469},
publisher = {Springer},
title = {Weighted iterated linear control},
volume = {56},
year = {2019},
bdsk-file-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxBbLi4vLi4vLi4vTGlicmFyeS9Nb2JpbGUgRG9jdW1lbnRzL2NvbX5hcHBsZX5DbG91ZERvY3MvQmlibGlvL0FydGljbGVzL0Z1bG9wVm9nbGVyMTlhY3RhLnBkZk8RAcQAAAAAAcQAAgAAB3N5c3RlbWUAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAABCRAAB/////xVGdWxvcFZvZ2xlcjE5YWN0YS5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAD/////AAAAAAAAAAAAAAAAAAMABgAACiBjdQAAAAAAAAAAAAAAAAAIQXJ0aWNsZXMAAgBjLzpVc2VyczpqYWNxdWVtYTpMaWJyYXJ5Ok1vYmlsZSBEb2N1bWVudHM6Y29tfmFwcGxlfkNsb3VkRG9jczpCaWJsaW86QXJ0aWNsZXM6RnVsb3BWb2dsZXIxOWFjdGEucGRmAAAOACwAFQBGAHUAbABvAHAAVgBvAGcAbABlAHIAMQA5AGEAYwB0AGEALgBwAGQAZgAPABAABwBzAHkAcwB0AGUAbQBlABIAYVVzZXJzL2phY3F1ZW1hL0xpYnJhcnkvTW9iaWxlIERvY3VtZW50cy9jb21+YXBwbGV+Q2xvdWREb2NzL0JpYmxpby9BcnRpY2xlcy9GdWxvcFZvZ2xlcjE5YWN0YS5wZGYAABMAAS8AABUAAgAP//8AAAAIAA0AGgAkAIIAAAAAAAACAQAAAAAAAAAFAAAAAAAAAAAAAAAAAAACSg==},
bdsk-url-1 = {https://doi.org/10.1007/s00236-018-0325-x}}
@book{Verovio,
date-added = {2021-05-11 12:20:16 +0200},
date-modified = {2021-05-11 12:20:16 +0200},
doi = {10.5448/7em6-my23},
publisher = {RISM, FNSNF},
title = {Verovio Reference Book},
url = {https://book.verovio.org/verovio-reference-book.pdf},
year = {2021},
bdsk-url-1 = {https://book.verovio.org/verovio-reference-book.pdf},
bdsk-url-2 = {https://doi.org/10.5448/7em6-my23}}
@article{Morbitz19multiop,
author = {M{\"o}rbitz, Richard and Vogler, Heiko},
date-added = {2021-05-11 11:50:58 +0200},
date-modified = {2021-05-11 11:51:51 +0200},
journal = {arXiv preprint arXiv:1911.06585},
title = {Weighted Parsing for Grammar-Based Language Models over Multioperator Monoids},
year = {2019},
bdsk-file-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxBaLi4vLi4vLi4vTGlicmFyeS9Nb2JpbGUgRG9jdW1lbnRzL2NvbX5hcHBsZX5DbG91ZERvY3MvQmlibGlvL0FydGljbGVzL01vcmJpdHoxOW11bHRpb3AucGRmTxEBvgAAAAABvgACAAAHc3lzdGVtZQAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAEJEAAH/////FE1vcmJpdHoxOW11bHRpb3AucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAP////8AAAAAAAAAAAAAAAAAAwAGAAAKIGN1AAAAAAAAAAAAAAAAAAhBcnRpY2xlcwACAGIvOlVzZXJzOmphY3F1ZW1hOkxpYnJhcnk6TW9iaWxlIERvY3VtZW50czpjb21+YXBwbGV+Q2xvdWREb2NzOkJpYmxpbzpBcnRpY2xlczpNb3JiaXR6MTltdWx0aW9wLnBkZgAOACoAFABNAG8AcgBiAGkAdAB6ADEAOQBtAHUAbAB0AGkAbwBwAC4AcABkAGYADwAQAAcAcwB5AHMAdABlAG0AZQASAGBVc2Vycy9qYWNxdWVtYS9MaWJyYXJ5L01vYmlsZSBEb2N1bWVudHMvY29tfmFwcGxlfkNsb3VkRG9jcy9CaWJsaW8vQXJ0aWNsZXMvTW9yYml0ejE5bXVsdGlvcC5wZGYAEwABLwAAFQACAA///wAAAAgADQAaACQAgQAAAAAAAAIBAAAAAAAAAAUAAAAAAAAAAAAAAAAAAAJD}}
@book{BaierKatoen08MC,
abstract = {Our growing dependence on increasingly complex computer and software systems necessitates the development of formalisms, techniques, and tools for assessing functional properties of these systems. One such technique that has emerged in the last twenty years is model checking, which systematically (and automatically) checks whether a model of a given system satisfies a desired property such as deadlock freedom, invariants, or request-response properties. This automated technique for verification and debugging has developed into a mature and widely used approach with many applications. Principles of Model Checking offers a comprehensive introduction to model checking that is not only a text suitable for classroom use but also a valuable reference for researchers and practitioners in the field.
The book begins with the basic principles for modeling concurrent and communicating systems, introduces different classes of properties (including safety and liveness), presents the notion of fairness, and provides automata-based algorithms for these properties. It introduces the temporal logics LTL and CTL, compares them, and covers algorithms for verifying these logics, discussing real-time systems as well as systems subject to random phenomena. Separate chapters treat such efficiency-improving techniques as abstraction and symbolic manipulation. The book includes an extensive set of examples (most of which run through several chapters) and a complete set of basic results accompanied by detailed proofs. Each chapter concludes with a summary, bibliographic notes, and an extensive list of exercises of both practical and theoretical nature.},
annote = {Contents
Foreword xiii
Preface xv
1 System Verification 1
1.1 Model Checking.................................. 7
1.2 Characteristics of Model Checking ....................... 11
1.2.1 The Model-Checking Process ...................... 11
1.2.2 Strengths and Weaknesses........................ 14
1.3 Bibliographic Notes................................ 16
2 Modelling Concurrent Systems 19
2.1 Transition Systems................................ 19
2.1.1 Executions ................................ 24
2.1.2 Modeling Hardware and Software Systems. . . . . . . . . . . . . . . 26
2.2 Parallelism and Communication......................... 35
2.2.1 Concurrency and Interleaving...................... 36
2.2.2 Communication via Shared Variables.................. 39
2.2.3 Handshaking ............................... 47
2.2.4 Channel Systems............................. 53
2.2.5 Nano Promela............................... 63
2.2.6 Synchronous Parallelism......................... 75
2.3 The State-Space Explosion Problem ...................... 77
2.4 Summary ..................................... 80
2.5 Bibliographic Notes................................ 80
2.6 Exercises ..................................... 82
3 Linear-Time Properties 89
3.1 Deadlock ..................................... 89
3.2 Linear-TimeBehavior .............................. 94
3.2.1 Pathsand State Graph ......................... 95
3.2.2 Traces................................... 97
3.2.3 Linear-TimeProperties .........................100
3.2.4 Trace Equivalence and Linear-Time Properties . . . . . . . . . . . . 104
3.3 Safety Properties and Invariants ........................107
3.3.1 Invariants.................................107
3.3.2 Safety Properties.............................111
3.3.3 Trace Equivalence and Safety Properties. . . . . . . . . . . . . . . .116
3.4 Liveness Properties................................120
3.4.1 Liveness Properties............................121
3.4.2 Safety vs. Liveness Properties......................122
3.5 Fairness ......................................126
3.5.1 FairnessConstraints ...........................129
3.5.2 FairnessStrategies ............................137
3.5.3 FairnessandSafety............................139
3.6 Summary .....................................141
3.7 Bibliographic Notes................................143
3.8 Exercises .....................................144
4 Regular Properties 151
4.1 Automata on Finite Words ...........................151
4.2 Model-Checking Regular Safety Properties. . . . . . . . . . . . . . . . . . .159
4.2.1 RegularSafetyProperties ........................159
4.2.2 VerifyingRegularSafetyProperties. . . . . . . . . . . . . . . . . . .163
4.3 Automata on Infinite Words...........................170
4.3.1 ω-Regular Languages and Properties..................170
4.3.2 Non deterministic B{\"u}chi Automata ...................173
4.3.3 Deterministic B{\"u}chi Automata .....................188
4.3.4 Generalized B{\"u}chi Automata ......................192
4.4 Model-Checking ω-Regular Properties .....................198
4.4.1 Persistence Properties and Product. . . . . . . . . . . . . . . . . . .199
4.4.2 Nested Depth-First Search........................203
4.5 Summary .....................................217
4.6 BibliographicNotes................................218
4.7 Exercises .....................................219
5 Linear Temporal Logic 229
5.1 Linear Temporal Logic..............................229
5.1.1 Syntax...................................231
5.1.2 Semantics.................................235
5.1.3 SpecifyingProperties...........................239
5.1.4 EquivalenceofLTLFormulae......................247
5.1.5 WeakUntil,Release,andPositiveNormalForm . . . . . . . . . . .252
5.1.6 FairnessinLTL..............................257
5.2 Automata-Based LTL ModelChecking.....................270
5.2.1 Complexity of the LTL Model-Checking Problem . . . . . . . . . . . 287
5.2.2 LTL Satisfiability and Validity Checking................296
5.3 Summary .....................................298
5.4 BibliographicNotes................................299
5.5 Exercises .....................................300
6 Computation Tree Logic 313
6.1 Introduction....................................313
6.2 Computation Tree Logic.............................317
6.2.1 Syntax...................................317
6.2.2 Semantics.................................320
6.2.3 Equivalence of CTL Formulae......................329
6.2.4 Normal Forms for CTL .........................332
6.3 Expressiveness of CTL vs. LTL .........................334
6.4 CTL Model Checking ..............................341
6.4.1 Basic Algorithm .............................341
6.4.2 The Until and Existential Always Operator . . . . . . . . . . . . . .347
6.4.3 Time and Space Complexity.......................355
6.5 Fairness in CTL .................................358
6.6 Counter examples and Witnesses ........................373
6.6.1 Counter examples in CTL ........................376
6.6.2 Counter examples and Witnesses in CTL with Fairness . . . . . . . . 380
6.7 Symbolic CTL Model Checking.........................381
6.7.1 Switching Functions ...........................382
6.7.2 Encoding Transition Systems by Switching Functions . . . . . . . . . 386
6.7.3 Ordered Binary Decision Diagrams...................392
6.7.4 Implementation of ROBDD-Based Algorithms . . . . . . . . . . . . 407
6.8 CTL∗ .......................................422
6.8.1 Logic,Expressiveness,andEquivalence. . . . . . . . . . . . . . . . .422
6.8.2 CTL∗ModelChecking..........................427
6.9 Summary .....................................430
6.10 Bibliographic Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 431
6.11Exercises .....................................433
7 Equivalences and Abstraction 449
7.1 Bisimulation....................................451
7.1.1 Bisimulation Quotient ..........................456
7.1.2 Action-Based Bisimulation .......................465
7.2 Bisimulation and CTL∗Equivalence ......................468
7.3 Bisimulation-Quotienting Algorithms......................476
7.3.1 DeterminingtheInitialPartition ....................478
7.3.2 RefiningPartitions............................480
7.3.3 A First Partition Refinement Algorithm . . . . . . . . . . . . . . . .486
7.3.4 An Efficiency Improvement .......................487
7.3.5 Equivalence Checking of Transition Systems. . . . . . . . . . . . . .493
7.4 Simulation Relations...............................496
7.4.1 SimulationEquivalence .........................505
7.4.2 Bisimulation, Simulation, and Trace Equivalence . . . . . . . . . . . 510
7.5 Simulation and ∀CTL∗Equivalence.......................515
7.6 Simulation-Quotienting Algorithms.......................521
7.7 Stutter Linear-Time Relations..........................529
7.7.1 Stutter Trace Equivalence........................530
7.7.2 Stutter Trace and LTL\⃝ Equivalence .................534
7.8 Stutter Bisimulation ...............................536
7.8.1 Divergence-Sensitive Stutter Bisimulation . . . . . . . . . . . . . . . 543
7.8.2 Normed Bisimulation...........................552
7.8.3 Stutter Bisimulation and CTL∗\⃝ Equivalence . . . . . . . . . . . . . 560
7.8.4 Stutter Bisimulation Quotienting....................567
7.9 Summary .....................................579
7.10 Bibliographic Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 580
7.11Exercises .....................................582
8 Partial Order Reduction 595
8.1 Independence of Actions.............................598
8.2 The Linear-Time Ample Set Approach.....................605
8.2.1 Ample Set Constraints..........................606
8.2.2 Dynamic Partial Order Reduction ...................619
8.2.3 Computing Ample Sets .........................627
8.2.4 StaticPartialOrderReduction .....................635
8.3 The Branching-Time Ample Set Approach...................650
8.4 Summary .....................................661
8.5 BibliographicNotes................................661
8.6 Exercises .....................................663
9 Timed Automata 673
9.1 Timed Automata.................................677
9.1.1 Semantics.................................684
9.1.2 Time Divergence, Timelock, and Zenoness...............690
9.2 Timed Computation Tree Logic.........................698
9.3 TCTL Model Checking..............................705
9.3.1 Eliminating Timing Parameters.....................706
9.3.2 Region Transition Systems .......................709
9.3.3 The TCTL Model-Checking Algorithm. . . . . . . . . . . . . . . . .732
9.4 Summary .....................................738
9.5 BibliographicNotes................................739
9.6 Exercises .....................................740
10 Probabilistic Systems 745
10.1Markov Chains ..................................747
10.1.1 Reachability Probabilities ........................759
10.1.2 Qualitative Properties ..........................770
10.2 Probabilistic Computation Tree Logic .....................780
10.2.1 PCTL Model Checking .........................785
10.2.2 The Qualitative Fragment of PCTL ..................787
10.3Linear-TimeProperties .............................796
10.4 PCTL∗ and Probabilistic Bisimulation . . . . . . . . . . . . . . . . . . . . . 806
10.4.1 PCTL∗ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 806
10.4.2 Probabilistic Bisimulation . . . . . . . . . . . . . . . . . . . . . . . . 808
10.5 Markov Chains with Costs . . . . . . . . . . . . . . . . . . . . . . . . . . . . 816
10.5.1 Cost-Bounded Reachability .......................818
10.5.2 Long-Run Properties...........................827
10.6 Markov Decision Processes . . . . . . . . . . . . . . . . . . . . . . . . . . . . 832
10.6.1 Reachability Probabilities ........................851
10.6.2 PCTL Model Checking .........................866
10.6.3 Limiting Properties ...........................869
10.6.4 Linear-Time Properties and PCTL∗ ..................880
10.6.5 Fairness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 883
10.7 Summary .....................................894
10.8 Bibliographic Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 896
10.9 Exercises .....................................899
A Appendix: Preliminaries 909
A.1 Frequently Used Symbols and Notations ....................909
A.2 Formal Languages ................................912
A.3 Propositional Logic................................915
A.4 Graphs.......................................920 A.5 ComputationalComplexity ...........................925
},
author = {Baier, Christel and Katoen, Joost-Pieter},
date-added = {2021-05-11 11:40:44 +0200},
date-modified = {2021-05-11 11:40:44 +0200},
isbn = {978-0-262-02649-9},
publisher = {MIT Press},
title = {Principles of Model Checking},
url = {http://mitpress.mit.edu/catalog/item/default.asp?ttype=2&tid=11481},
year = {2008},
bdsk-file-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxBfLi4vLi4vLi4vTGlicmFyeS9Nb2JpbGUgRG9jdW1lbnRzL2NvbX5hcHBsZX5DbG91ZERvY3MvQmlibGlvL0Jvb2tzL0JhaWVyS2F0b2VuLVByaW5jaXBsZXNNQy5wZGZPEQHYAAAAAAHYAAIAAAdzeXN0ZW1lAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAQkQAAf////8cQmFpZXJLYXRvZW4tUHJpbmNpcGxlc01DLnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA/////wAAAAAAAAAAAAAAAAADAAYAAAogY3UAAAAAAAAAAAAAAAAABUJvb2tzAAACAGcvOlVzZXJzOmphY3F1ZW1hOkxpYnJhcnk6TW9iaWxlIERvY3VtZW50czpjb21+YXBwbGV+Q2xvdWREb2NzOkJpYmxpbzpCb29rczpCYWllckthdG9lbi1QcmluY2lwbGVzTUMucGRmAAAOADoAHABCAGEAaQBlAHIASwBhAHQAbwBlAG4ALQBQAHIAaQBuAGMAaQBwAGwAZQBzAE0AQwAuAHAAZABmAA8AEAAHAHMAeQBzAHQAZQBtAGUAEgBlVXNlcnMvamFjcXVlbWEvTGlicmFyeS9Nb2JpbGUgRG9jdW1lbnRzL2NvbX5hcHBsZX5DbG91ZERvY3MvQmlibGlvL0Jvb2tzL0JhaWVyS2F0b2VuLVByaW5jaXBsZXNNQy5wZGYAABMAAS8AABUAAgAP//8AAAAIAA0AGgAkAIYAAAAAAAACAQAAAAAAAAAFAAAAAAAAAAAAAAAAAAACYg==},
bdsk-url-1 = {http://mitpress.mit.edu/catalog/item/default.asp?ttype=2&tid=11481}}
@inproceedings{Vardi07ciaa,
author = {Vardi, Moshe Y},
booktitle = {International Conference on Implementation and Application of Automata},
date-added = {2021-05-11 11:29:21 +0200},
date-modified = {2021-05-11 11:29:21 +0200},
organization = {Springer},
pages = {5--10},
title = {Linear-time model checking: automata theory in practice},
year = {2007},
bdsk-file-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxBULi4vLi4vLi4vTGlicmFyeS9Nb2JpbGUgRG9jdW1lbnRzL2NvbX5hcHBsZX5DbG91ZERvY3MvQmlibGlvL1N1cnZleXMvVmFyZGkwN2NpYWEucGRmTxEBqAAAAAABqAACAAAHc3lzdGVtZQAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAEJEAAH/////D1ZhcmRpMDdjaWFhLnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAP////8AAAAAAAAAAAAAAAAAAwAGAAAKIGN1AAAAAAAAAAAAAAAAAAdTdXJ2ZXlzAAACAFwvOlVzZXJzOmphY3F1ZW1hOkxpYnJhcnk6TW9iaWxlIERvY3VtZW50czpjb21+YXBwbGV+Q2xvdWREb2NzOkJpYmxpbzpTdXJ2ZXlzOlZhcmRpMDdjaWFhLnBkZgAOACAADwBWAGEAcgBkAGkAMAA3AGMAaQBhAGEALgBwAGQAZgAPABAABwBzAHkAcwB0AGUAbQBlABIAWlVzZXJzL2phY3F1ZW1hL0xpYnJhcnkvTW9iaWxlIERvY3VtZW50cy9jb21+YXBwbGV+Q2xvdWREb2NzL0JpYmxpby9TdXJ2ZXlzL1ZhcmRpMDdjaWFhLnBkZgATAAEvAAAVAAIAD///AAAACAANABoAJAB7AAAAAAAAAgEAAAAAAAAABQAAAAAAAAAAAAAAAAAAAic=}}
@inproceedings{Allauzen07openfst,
author = {Allauzen, Cyril and Riley, Michael and Schalkwyk, Johan and Skut, Wojciech and Mohri, Mehryar},
booktitle = {International Conference on Implementation and Application of Automata},
date-added = {2021-05-11 11:29:04 +0200},
date-modified = {2021-05-11 11:29:04 +0200},
organization = {Springer},
pages = {11--23},
title = {OpenFst: A general and efficient weighted finite-state transducer library},
year = {2007},
bdsk-file-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxBbLi4vLi4vLi4vTGlicmFyeS9Nb2JpbGUgRG9jdW1lbnRzL2NvbX5hcHBsZX5DbG91ZERvY3MvQmlibGlvL0FydGljbGVzL0FsbGF1emVuMDdvcGVuZnN0LnBkZk8RAcQAAAAAAcQAAgAAB3N5c3RlbWUAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAABCRAAB/////xVBbGxhdXplbjA3b3BlbmZzdC5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAD/////AAAAAAAAAAAAAAAAAAMABgAACiBjdQAAAAAAAAAAAAAAAAAIQXJ0aWNsZXMAAgBjLzpVc2VyczpqYWNxdWVtYTpMaWJyYXJ5Ok1vYmlsZSBEb2N1bWVudHM6Y29tfmFwcGxlfkNsb3VkRG9jczpCaWJsaW86QXJ0aWNsZXM6QWxsYXV6ZW4wN29wZW5mc3QucGRmAAAOACwAFQBBAGwAbABhAHUAegBlAG4AMAA3AG8AcABlAG4AZgBzAHQALgBwAGQAZgAPABAABwBzAHkAcwB0AGUAbQBlABIAYVVzZXJzL2phY3F1ZW1hL0xpYnJhcnkvTW9iaWxlIERvY3VtZW50cy9jb21+YXBwbGV+Q2xvdWREb2NzL0JpYmxpby9BcnRpY2xlcy9BbGxhdXplbjA3b3BlbmZzdC5wZGYAABMAAS8AABUAAgAP//8AAAAIAA0AGgAkAIIAAAAAAAACAQAAAAAAAAAFAAAAAAAAAAAAAAAAAAACSg==}}
@inproceedings{Benedikt10logic,
author = {Benedikt, Michael and Ley, Clemens and Puppis, Gabriele},
booktitle = {International Workshop on Computer Science Logic},
date-added = {2021-05-10 22:11:20 +0200},
date-modified = {2021-05-10 22:11:20 +0200},
organization = {Springer},
pages = {110--124},
title = {Automata vs. logics on data words},
year = {2010}}
@article{Bouyer03algebraic,
author = {Bouyer, Patricia and Petit, Antoine and Th{\'e}rien, Denis},
date-added = {2021-05-10 22:03:43 +0200},
date-modified = {2021-05-10 22:03:43 +0200},
journal = {Information and Computation},
number = {2},
pages = {137--162},
publisher = {Elsevier},
title = {An algebraic approach to data languages and timed languages},
volume = {182},
year = {2003},
bdsk-file-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxBWLi4vLi4vLi4vTGlicmFyeS9Nb2JpbGUgRG9jdW1lbnRzL2NvbX5hcHBsZX5DbG91ZERvY3MvQmlibGlvL0FydGljbGVzL0JvdXllcjAzZGF0YS5wZGZPEQGuAAAAAAGuAAIAAAdzeXN0ZW1lAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAQkQAAf////8QQm91eWVyMDNkYXRhLnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA/////wAAAAAAAAAAAAAAAAADAAYAAAogY3UAAAAAAAAAAAAAAAAACEFydGljbGVzAAIAXi86VXNlcnM6amFjcXVlbWE6TGlicmFyeTpNb2JpbGUgRG9jdW1lbnRzOmNvbX5hcHBsZX5DbG91ZERvY3M6QmlibGlvOkFydGljbGVzOkJvdXllcjAzZGF0YS5wZGYADgAiABAAQgBvAHUAeQBlAHIAMAAzAGQAYQB0AGEALgBwAGQAZgAPABAABwBzAHkAcwB0AGUAbQBlABIAXFVzZXJzL2phY3F1ZW1hL0xpYnJhcnkvTW9iaWxlIERvY3VtZW50cy9jb21+YXBwbGV+Q2xvdWREb2NzL0JpYmxpby9BcnRpY2xlcy9Cb3V5ZXIwM2RhdGEucGRmABMAAS8AABUAAgAP//8AAAAIAA0AGgAkAH0AAAAAAAACAQAAAAAAAAAFAAAAAAAAAAAAAAAAAAACLw==}}
@article{Bojanczyk11FO2,
author = {Boja{\'n}czyk, Miko{\l}aj and David, Claire and Muscholl, Anca and Schwentick, Thomas and Segoufin, Luc},
date-added = {2021-05-10 22:01:33 +0200},
date-modified = {2021-05-10 22:01:50 +0200},
journal = {ACM Transactions on Computational Logic (TOCL)},
number = {4},
pages = {1--26},
publisher = {ACM New York, NY, USA},
title = {Two-variable logic on data words},
volume = {12},
year = {2011}}
@article{KaminskiFrancez94,
acmid = {194534},
address = {Essex, UK},
author = {Kaminski, Michael and Francez, Nissim},
date-added = {2021-05-10 22:00:06 +0200},
date-modified = {2021-10-15 11:50:34 +0200},
issn = {0304-3975},
issue = {2},
journal = {Theoretical Computer Science},
month = {November},
numpages = {35},
pages = {329--363},
publisher = {Elsevier Science Publishers Ltd.},
title = {Finite-memory automata},
volume = {134},
year = {1994},
bdsk-url-1 = {http://dx.doi.org/10.1016/0304-3975(94)90242-9}}
@article{NevenSchwentickVianu04FSMinfinite,
abstract = {Motivated by formal models recently proposed in the context of XML, we study automata and logics on strings over infinite alphabets.
These are conservative extensions of classical automata and logics defining the regular languages on finite alphabets.
Specifically, we consider register and pebble automata, and extensions of first-order logic and monadic second-order logic.
For each type of automaton we consider one-way and two-way variants, as well as deterministic, nondeterministic, and alternating control.
We investigate the expressiveness and complexity of the automata and their connection to the logics, as well as standard decision problems.
Some of our results answer open questions of Kaminski and Francez on register automata.},
acmid = {1013562},
address = {New York, NY, USA},
author = {Neven, Frank and Schwentick, Thomas and Vianu, Victor},
date-added = {2021-05-10 21:57:52 +0200},
date-modified = {2021-10-15 11:52:50 +0200},
issn = {1529-3785},
journal = {ACM Trans. Comput. Logic},
keywords = {automata theory, XML, expressiveness, first-order logic, infinite alphabets, monadic second-order logic, pebbles, registers},
month = jul,
number = {3},
numpages = {33},
pages = {403--435},
publisher = {ACM},
title = {Finite state machines for strings over infinite alphabets},
volume = {5},
year = {2004},
bdsk-url-1 = {http://doi.acm.org/10.1145/1013560.1013562},
bdsk-url-2 = {http://dx.doi.org/10.1145/1013560.1013562}}
@inproceedings{foscarin:hal-01988990,
author = {Foscarin, Francesco and Jacquemard, Florent and Rigaux, Philippe and Sakai, Masahiko},
booktitle = {Mathematics and Computation in Music (MCM)},
date-added = {2021-05-10 19:51:03 +0200},
date-modified = {2021-10-15 11:48:24 +0200},
pdf = {https://hal.inria.fr/hal-01988990v2/file/springer12.pdf},
publisher = {{Springer}},
series = {LNAI},
title = {{A Parse-based Framework for Coupled Rhythm Quantization and Score Structuring}},
volume = {11502},
year = {2019},
bdsk-url-1 = {https://hal.inria.fr/hal-01988990},
bdsk-url-2 = {https://doi.org/10.1007/978-3-030-21392-3%5C_20}}
@book{tata,
author = {Comon, Hubert and Dauchet, Max and Gilleron, R{\'e}mi and Jacquemard, Florent and L{\"o}ding, Christoph and Lugiez, Denis and Tison, Sophie and Tommasi, Marc},
date-added = {2021-05-10 19:45:13 +0200},
date-modified = {2021-05-10 19:45:13 +0200},
publisher = {\url{http://tata.gforge.inria.fr}},
title = {{Tree Automata Techniques and Applications}},
year = {2007},
bdsk-file-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxBLLi4vLi4vLi4vTGlicmFyeS9Nb2JpbGUgRG9jdW1lbnRzL2NvbX5hcHBsZX5DbG91ZERvY3MvQmlibGlvL0Jvb2tzL3RhdGEucGRmTxEBiAAAAAABiAACAAAHc3lzdGVtZQAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAEJEAAH/////CHRhdGEucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAP////8AAAAAAAAAAAAAAAAAAwAGAAAKIGN1AAAAAAAAAAAAAAAAAAVCb29rcwAAAgBTLzpVc2VyczpqYWNxdWVtYTpMaWJyYXJ5Ok1vYmlsZSBEb2N1bWVudHM6Y29tfmFwcGxlfkNsb3VkRG9jczpCaWJsaW86Qm9va3M6dGF0YS5wZGYAAA4AEgAIAHQAYQB0AGEALgBwAGQAZgAPABAABwBzAHkAcwB0AGUAbQBlABIAUVVzZXJzL2phY3F1ZW1hL0xpYnJhcnkvTW9iaWxlIERvY3VtZW50cy9jb21+YXBwbGV+Q2xvdWREb2NzL0JpYmxpby9Cb29rcy90YXRhLnBkZgAAEwABLwAAFQACAA///wAAAAgADQAaACQAcgAAAAAAAAIBAAAAAAAAAAUAAAAAAAAAAAAAAAAAAAH+},
bdsk-file-2 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxBXLi4vLi4vLi4vTGlicmFyeS9Nb2JpbGUgRG9jdW1lbnRzL2NvbX5hcHBsZX5DbG91ZERvY3MvQmlibGlvL0FydGljbGVzL1RBVEEgMjMtMzItMjgucGRmTxEBtAAAAAABtAACAAAHc3lzdGVtZQAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAEJEAAH/////EVRBVEEgMjMtMzItMjgucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAP////8AAAAAAAAAAAAAAAAAAwAGAAAKIGN1AAAAAAAAAAAAAAAAAAhBcnRpY2xlcwACAF8vOlVzZXJzOmphY3F1ZW1hOkxpYnJhcnk6TW9iaWxlIERvY3VtZW50czpjb21+YXBwbGV+Q2xvdWREb2NzOkJpYmxpbzpBcnRpY2xlczpUQVRBIDIzLTMyLTI4LnBkZgAADgAkABEAVABBAFQAQQAgADIAMwAtADMAMgAtADIAOAAuAHAAZABmAA8AEAAHAHMAeQBzAHQAZQBtAGUAEgBdVXNlcnMvamFjcXVlbWEvTGlicmFyeS9Nb2JpbGUgRG9jdW1lbnRzL2NvbX5hcHBsZX5DbG91ZERvY3MvQmlibGlvL0FydGljbGVzL1RBVEEgMjMtMzItMjgucGRmAAATAAEvAAAVAAIAD///AAAACAANABoAJAB+AAAAAAAAAgEAAAAAAAAABQAAAAAAAAAAAAAAAAAAAjY=}}
@inproceedings{Segoufin06csl,
author = {Segoufin, Luc},
booktitle = {Computer Science Logic},
date-added = {2021-05-10 19:40:24 +0200},
date-modified = {2021-05-10 19:40:24 +0200},
publisher = {Springer},
series = {LNCS},
title = {Automata and Logics for Words and Trees over an Infinite Alphabet},
volume = 4207,
year = 2006,
bdsk-file-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxBWLi4vLi4vLi4vTGlicmFyeS9Nb2JpbGUgRG9jdW1lbnRzL2NvbX5hcHBsZX5DbG91ZERvY3MvQmlibGlvL1N1cnZleXMvU2Vnb3VmaW4wNmNzbC5wZGZPEQGwAAAAAAGwAAIAAAdzeXN0ZW1lAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAQkQAAf////8RU2Vnb3VmaW4wNmNzbC5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA/////wAAAAAAAAAAAAAAAAADAAYAAAogY3UAAAAAAAAAAAAAAAAAB1N1cnZleXMAAAIAXi86VXNlcnM6amFjcXVlbWE6TGlicmFyeTpNb2JpbGUgRG9jdW1lbnRzOmNvbX5hcHBsZX5DbG91ZERvY3M6QmlibGlvOlN1cnZleXM6U2Vnb3VmaW4wNmNzbC5wZGYADgAkABEAUwBlAGcAbwB1AGYAaQBuADAANgBjAHMAbAAuAHAAZABmAA8AEAAHAHMAeQBzAHQAZQBtAGUAEgBcVXNlcnMvamFjcXVlbWEvTGlicmFyeS9Nb2JpbGUgRG9jdW1lbnRzL2NvbX5hcHBsZX5DbG91ZERvY3MvQmlibGlvL1N1cnZleXMvU2Vnb3VmaW4wNmNzbC5wZGYAEwABLwAAFQACAA///wAAAAgADQAaACQAfQAAAAAAAAIBAAAAAAAAAAUAAAAAAAAAAAAAAAAAAAIx}}
@inproceedings{Segoufin02streaming,
author = {Segoufin, Luc and Vianu, Victor},
booktitle = {Proceedings of the twenty-first ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems},
date-added = {2021-05-10 19:05:35 +0200},
date-modified = {2021-05-10 19:05:35 +0200},
pages = {53--64},
title = {Validating streaming XML documents},
year = {2002}}
@book{GruneJacobs08parsing,
abstract = {Parsing, also referred to as syntax analysis, has been and continues to be an essential part of computer science and linguistics. Today, parsing is also applied in other disciplines; some examples are document preparation and conversion, chemical formulae typesetting, and chromosome recognition.
In addition to the traditional parsing techniques, this second edition presents new developments and discoveries: generalized deterministic parsing, linear-time substring parsing, parallel parsing, parsing as intersection, non-canonical methods, non-Chomsky systems, and many more.
Parsing techniques provide a solid basis for compiler construction and linguistics, and contribute to all existing software: they enable Web browsers to analyze HTML pages and PostScript printers to analyze PostScript, and some of the more advanced techniques are used in code generation in compilers and in data compression. Also their importance as general pattern recognizers is slowly being acknowledged.
To provide readers with low-threshold access to the full field of parsing techniques, this book uses a two-tiered structure. The basic ideas behind the existing parsing techniques are explained in an intuitive and narrative style, starting from the first principles of data structures and algorithms; this provides breadth and accessibility. The hundreds of realizations and improvements of these basic ideas are explained in an extensive annotated bibliography, in a much terser, yet still informal style; this provides depth.
The reader should have an understanding of algorithmic thinking, especially recursion; however, knowledge of any particular programming language is not required.
},
annote = {Originally published by Ellis Horwood Ltd, Prentice Hall, UK, 1990},
author = {Grune, Dick and Jacobs, Ceriel J.H.},
date-added = {2021-05-10 16:31:49 +0200},
date-modified = {2021-05-10 18:36:16 +0200},
isbn = {978-1-4419-1901-4},
number = {2nd edition},
publisher = {Springer},
series = {Monographs in Computer Science},
title = {Parsing Techniques},
year = {2008},
bdsk-file-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxBVLi4vLi4vLi4vRHJvcGJveC9TaGFyZWQvQXV0b21hdGljIE11c2ljIFRyYW5zY3JpcHRpb24vUGFyc2luZy9HcnVuZUphY29icy1QYXJzaW5nLnBkZk8RAbwAAAAAAbwAAgAAB3N5c3RlbWUAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAABCRAAB/////xdHcnVuZUphY29icy1QYXJzaW5nLnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAD/////AAAAAAAAAAAAAAAAAAMABQAACiBjdQAAAAAAAAAAAAAAAAAHUGFyc2luZwAAAgBdLzpVc2VyczpqYWNxdWVtYTpEcm9wYm94OlNoYXJlZDpBdXRvbWF0aWMgTXVzaWMgVHJhbnNjcmlwdGlvbjpQYXJzaW5nOkdydW5lSmFjb2JzLVBhcnNpbmcucGRmAAAOADAAFwBHAHIAdQBuAGUASgBhAGMAbwBiAHMALQBQAGEAcgBzAGkAbgBnAC4AcABkAGYADwAQAAcAcwB5AHMAdABlAG0AZQASAFtVc2Vycy9qYWNxdWVtYS9Ecm9wYm94L1NoYXJlZC9BdXRvbWF0aWMgTXVzaWMgVHJhbnNjcmlwdGlvbi9QYXJzaW5nL0dydW5lSmFjb2JzLVBhcnNpbmcucGRmAAATAAEvAAAVAAIAD///AAAACAANABoAJAB8AAAAAAAAAgEAAAAAAAAABQAAAAAAAAAAAAAAAAAAAjw=}}
@incollection{Kuich97semirings,
author = {Kuich, Werner},
booktitle = {Handbook of formal languages},
date-added = {2021-05-10 11:43:11 +0200},
date-modified = {2021-05-10 11:43:20 +0200},
pages = {609--677},
publisher = {Springer},
title = {Semirings and formal power series: Their relevance to formal languages and automata},
year = {1997}}
@article{Goodman99semiring,
abstract = {We synthesize work on parsing algorithms, deductive parsing, and the theory of algebra applied toformal languages into ageneral systemfor describing parsers. Eachparserperforms abstract computations usingtheoperationsofasemiring. Thesystemallowsasingle,simplerepresentation to be used for describing parsers that compute recognition, derivation forests, Viterbi, n-best, inside values, and other values, simply by substituting the operations of different semirings. We also show how to use the same representation, interpreted differently, to compute outside values. The system can be used to describe a wide variety of parsers, including Earley's algorithm, tree adjoining grammar parsing, Graham Harrison Ruzzo parsing, and prefix value computation.},
author = {Goodman, Joshua},
date-added = {2021-05-10 11:41:01 +0200},
date-modified = {2021-05-10 11:45:16 +0200},
journal = {Computational Linguistics},
number = {4},
pages = {573--606},
title = {Semiring parsing},
volume = {25},
year = {1999},
bdsk-file-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxBbLi4vLi4vLi4vTGlicmFyeS9Nb2JpbGUgRG9jdW1lbnRzL2NvbX5hcHBsZX5DbG91ZERvY3MvQmlibGlvL0FydGljbGVzL0dvb2RtYW45OXNlbWlyaW5nLnBkZk8RAcQAAAAAAcQAAgAAB3N5c3RlbWUAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAABCRAAB/////xVHb29kbWFuOTlzZW1pcmluZy5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAD/////AAAAAAAAAAAAAAAAAAMABgAACiBjdQAAAAAAAAAAAAAAAAAIQXJ0aWNsZXMAAgBjLzpVc2VyczpqYWNxdWVtYTpMaWJyYXJ5Ok1vYmlsZSBEb2N1bWVudHM6Y29tfmFwcGxlfkNsb3VkRG9jczpCaWJsaW86QXJ0aWNsZXM6R29vZG1hbjk5c2VtaXJpbmcucGRmAAAOACwAFQBHAG8AbwBkAG0AYQBuADkAOQBzAGUAbQBpAHIAaQBuAGcALgBwAGQAZgAPABAABwBzAHkAcwB0AGUAbQBlABIAYVVzZXJzL2phY3F1ZW1hL0xpYnJhcnkvTW9iaWxlIERvY3VtZW50cy9jb21+YXBwbGV+Q2xvdWREb2NzL0JpYmxpby9BcnRpY2xlcy9Hb29kbWFuOTlzZW1pcmluZy5wZGYAABMAAS8AABUAAgAP//8AAAAIAA0AGgAkAIIAAAAAAAACAQAAAAAAAAAFAAAAAAAAAAAAAAAAAAACSg==}}
@inproceedings{Krebs16cost,
author = {Krebs, Andreas and Limaye, Nutan and Ludwig, Michael},
booktitle = {International Computing and Combinatorics Conference},
date-added = {2021-05-06 18:48:12 +0200},
date-modified = {2021-05-06 18:51:09 +0200},
keywords = {VPA},
organization = {Springer},
pages = {587--598},
title = {Cost register automata for nested words},
year = {2016},
bdsk-file-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxBVLi4vLi4vLi4vTGlicmFyeS9Nb2JpbGUgRG9jdW1lbnRzL2NvbX5hcHBsZX5DbG91ZERvY3MvQmlibGlvL0FydGljbGVzL0tyZWJzMTZjb3N0LnBkZk8RAawAAAAAAawAAgAAB3N5c3RlbWUAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAABCRAAB/////w9LcmViczE2Y29zdC5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAD/////AAAAAAAAAAAAAAAAAAMABgAACiBjdQAAAAAAAAAAAAAAAAAIQXJ0aWNsZXMAAgBdLzpVc2VyczpqYWNxdWVtYTpMaWJyYXJ5Ok1vYmlsZSBEb2N1bWVudHM6Y29tfmFwcGxlfkNsb3VkRG9jczpCaWJsaW86QXJ0aWNsZXM6S3JlYnMxNmNvc3QucGRmAAAOACAADwBLAHIAZQBiAHMAMQA2AGMAbwBzAHQALgBwAGQAZgAPABAABwBzAHkAcwB0AGUAbQBlABIAW1VzZXJzL2phY3F1ZW1hL0xpYnJhcnkvTW9iaWxlIERvY3VtZW50cy9jb21+YXBwbGV+Q2xvdWREb2NzL0JpYmxpby9BcnRpY2xlcy9LcmViczE2Y29zdC5wZGYAABMAAS8AABUAAgAP//8AAAAIAA0AGgAkAHwAAAAAAAACAQAAAAAAAAAFAAAAAAAAAAAAAAAAAAACLA==}}
@inproceedings{Caralp12VPAmult,
author = {Caralp, Mathieu and Reynier, Pierre-Alain and Talbot, Jean-Marc},
booktitle = {International Conference on Developments in Language Theory},
date-added = {2021-05-06 18:16:24 +0200},
date-modified = {2021-05-06 18:16:24 +0200},
organization = {Springer},
pages = {226--238},
title = {Visibly pushdown automata with multiplicities: finiteness and k-boundedness},
year = {2012},
bdsk-file-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxBZLi4vLi4vLi4vTGlicmFyeS9Nb2JpbGUgRG9jdW1lbnRzL2NvbX5hcHBsZX5DbG91ZERvY3MvQmlibGlvL0FydGljbGVzL0NhcmFscDEyVlBBbXVsdC5wZGZPEQG8AAAAAAG8AAIAAAdzeXN0ZW1lAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAQkQAAf////8TQ2FyYWxwMTJWUEFtdWx0LnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA/////wAAAAAAAAAAAAAAAAADAAYAAAogY3UAAAAAAAAAAAAAAAAACEFydGljbGVzAAIAYS86VXNlcnM6amFjcXVlbWE6TGlicmFyeTpNb2JpbGUgRG9jdW1lbnRzOmNvbX5hcHBsZX5DbG91ZERvY3M6QmlibGlvOkFydGljbGVzOkNhcmFscDEyVlBBbXVsdC5wZGYAAA4AKAATAEMAYQByAGEAbABwADEAMgBWAFAAQQBtAHUAbAB0AC4AcABkAGYADwAQAAcAcwB5AHMAdABlAG0AZQASAF9Vc2Vycy9qYWNxdWVtYS9MaWJyYXJ5L01vYmlsZSBEb2N1bWVudHMvY29tfmFwcGxlfkNsb3VkRG9jcy9CaWJsaW8vQXJ0aWNsZXMvQ2FyYWxwMTJWUEFtdWx0LnBkZgAAEwABLwAAFQACAA///wAAAAgADQAaACQAgAAAAAAAAAIBAAAAAAAAAAUAAAAAAAAAAAAAAAAAAAJA}}
@article{Worrell13equivalence,
author = {Worrell, James and Wachter, Bjoern and Ouaknine, Joel and Murawski, Andrzej and Kiefer, Stefan},
date-added = {2021-05-06 18:06:54 +0200},
date-modified = {2021-05-06 18:07:55 +0200},
journal = {Logical Methods in Computer Science},
publisher = {Episciences. org},
title = {On the Complexity of Equivalence and Minimisation for Q-weighted Automata},
volume = {9},
year = {2013},
bdsk-file-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxBXLi4vLi4vLi4vTGlicmFyeS9Nb2JpbGUgRG9jdW1lbnRzL2NvbX5hcHBsZX5DbG91ZERvY3MvQmlibGlvL0FydGljbGVzL1dvcnJlbGwxM1dWUEEucGRmTxEBtAAAAAABtAACAAAHc3lzdGVtZQAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAEJEAAH/////EVdvcnJlbGwxM1dWUEEucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAP////8AAAAAAAAAAAAAAAAAAwAGAAAKIGN1AAAAAAAAAAAAAAAAAAhBcnRpY2xlcwACAF8vOlVzZXJzOmphY3F1ZW1hOkxpYnJhcnk6TW9iaWxlIERvY3VtZW50czpjb21+YXBwbGV+Q2xvdWREb2NzOkJpYmxpbzpBcnRpY2xlczpXb3JyZWxsMTNXVlBBLnBkZgAADgAkABEAVwBvAHIAcgBlAGwAbAAxADMAVwBWAFAAQQAuAHAAZABmAA8AEAAHAHMAeQBzAHQAZQBtAGUAEgBdVXNlcnMvamFjcXVlbWEvTGlicmFyeS9Nb2JpbGUgRG9jdW1lbnRzL2NvbX5hcHBsZX5DbG91ZERvY3MvQmlibGlvL0FydGljbGVzL1dvcnJlbGwxM1dWUEEucGRmAAATAAEvAAAVAAIAD///AAAACAANABoAJAB+AAAAAAAAAgEAAAAAAAAABQAAAAAAAAAAAAAAAAAAAjY=}}
@article{Mohri03ijfcs,
author = {Mohri, Mehryar},
date-added = {2021-05-05 11:54:05 +0200},
date-modified = {2021-05-05 11:54:05 +0200},
journal = {International Journal of Foundations of Computer Science},
number = {06},
pages = {957--982},
publisher = {World Scientific},
title = {Edit-distance of weighted automata: General definitions and algorithms},
volume = {14},
year = {2003}}
@inproceedings{dAntoniVeanes17CAV,
author = {D'Antoni, Loris and Veanes, Margus},
booktitle = {International Conference on Computer Aided Verification},
date-added = {2021-05-04 10:33:30 +0200},
date-modified = {2021-05-04 10:33:44 +0200},
organization = {Springer},
pages = {47--67},
title = {The power of symbolic automata and transducers},
year = {2017},
bdsk-file-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxBfLi4vLi4vLi4vTGlicmFyeS9Nb2JpbGUgRG9jdW1lbnRzL2NvbX5hcHBsZX5DbG91ZERvY3MvQmlibGlvL1N1cnZleXMvZEFudG9uaVZlYW5lczE3Q0FWdHV0by5wZGZPEQHWAAAAAAHWAAIAAAdzeXN0ZW1lAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAQkQAAf////8aZEFudG9uaVZlYW5lczE3Q0FWdHV0by5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA/////wAAAAAAAAAAAAAAAAADAAYAAAogY3UAAAAAAAAAAAAAAAAAB1N1cnZleXMAAAIAZy86VXNlcnM6amFjcXVlbWE6TGlicmFyeTpNb2JpbGUgRG9jdW1lbnRzOmNvbX5hcHBsZX5DbG91ZERvY3M6QmlibGlvOlN1cnZleXM6ZEFudG9uaVZlYW5lczE3Q0FWdHV0by5wZGYAAA4ANgAaAGQAQQBuAHQAbwBuAGkAVgBlAGEAbgBlAHMAMQA3AEMAQQBWAHQAdQB0AG8ALgBwAGQAZgAPABAABwBzAHkAcwB0AGUAbQBlABIAZVVzZXJzL2phY3F1ZW1hL0xpYnJhcnkvTW9iaWxlIERvY3VtZW50cy9jb21+YXBwbGV+Q2xvdWREb2NzL0JpYmxpby9TdXJ2ZXlzL2RBbnRvbmlWZWFuZXMxN0NBVnR1dG8ucGRmAAATAAEvAAAVAAIAD///AAAACAANABoAJACGAAAAAAAAAgEAAAAAAAAABQAAAAAAAAAAAAAAAAAAAmA=}}
@article{dAntoni21CACM,
author = {D'Antoni, Loris and Veanes, Margus},
date-added = {2021-05-03 17:08:14 +0200},
date-modified = {2021-10-15 11:47:28 +0200},
journal = {Communications of the ACM},
number = {5},
pages = {86--95},
publisher = {ACM New York, NY, USA},
title = {Automata modulo theories},
url = {https://pages.cs.wisc.edu/~loris/symbolicautomata.html},
volume = {64},
year = {2021},
bdsk-file-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxBWLi4vLi4vLi4vTGlicmFyeS9Nb2JpbGUgRG9jdW1lbnRzL2NvbX5hcHBsZX5DbG91ZERvY3MvQmlibGlvL1N1cnZleXMvZEFudG9uaTIxQ0FDTS5wZGZPEQGwAAAAAAGwAAIAAAdzeXN0ZW1lAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAQkQAAf////8RZEFudG9uaTIxQ0FDTS5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA/////wAAAAAAAAAAAAAAAAADAAYAAAogY3UAAAAAAAAAAAAAAAAAB1N1cnZleXMAAAIAXi86VXNlcnM6amFjcXVlbWE6TGlicmFyeTpNb2JpbGUgRG9jdW1lbnRzOmNvbX5hcHBsZX5DbG91ZERvY3M6QmlibGlvOlN1cnZleXM6ZEFudG9uaTIxQ0FDTS5wZGYADgAkABEAZABBAG4AdABvAG4AaQAyADEAQwBBAEMATQAuAHAAZABmAA8AEAAHAHMAeQBzAHQAZQBtAGUAEgBcVXNlcnMvamFjcXVlbWEvTGlicmFyeS9Nb2JpbGUgRG9jdW1lbnRzL2NvbX5hcHBsZX5DbG91ZERvY3MvQmlibGlvL1N1cnZleXMvZEFudG9uaTIxQ0FDTS5wZGYAEwABLwAAFQACAA///wAAAAgADQAaACQAfQAAAAAAAAIBAAAAAAAAAAUAAAAAAAAAAAAAAAAAAAIx},
bdsk-url-1 = {see%20also%20see%20also%20https://pages.cs.wisc.edu/~loris/symbolicautomata.html}}
@book{Eilenberg74automata,
author = {Eilenberg, Samuel},
date-added = {2021-05-03 16:54:35 +0200},
date-modified = {2021-05-03 16:54:35 +0200},
number = {59},
publisher = {Academic press},
series = {Pure and Applied Mathematics},
title = {Automata, Languages, and Machines},
volume = {A},
year = {1974}}
@article{Goodman99SemiringParsing,
abstract = {We synthesize work on parsing algorithms, deductive parsing, and the theory of algebra applied to formal languages into a general system for describing parsers. Each parser performs abstract computations using the operations of a semiring. The system allows a single, simple representation to be used for describing parsers that compute recognition, derivation forests, Viterbi, n-best, inside values, and other values, simply by substituting the operations of different semirings. We also show how to use the same representation, interpreted differently, to compute outside values. The system can be used to describe a wide variety of parsers, including Earley's algorithm, tree adjoining grammar parsing, Graham Harrison Ruzzo parsing, and prefix value computation.},
author = {Goodman, Joshua},
date-added = {2021-05-03 16:48:57 +0200},
date-modified = {2021-05-03 16:49:30 +0200},
journal = {Computational Linguistics},
number = {4},
pages = {573--606},
title = {Semiring parsing},
volume = {25},
year = {1999}}
@incollection{Mahr84semirings,
author = {Mahr, Bernd},
booktitle = {North-Holland mathematics studies},
date-added = {2021-05-03 16:21:11 +0200},
date-modified = {2021-05-03 16:21:23 +0200},
pages = {229--256},
publisher = {Elsevier},
title = {Iteration and summability in semirings},
volume = {95},
year = {1984}}
@inproceedings{MorbitzVogler19weighted-parsing,
abstract = {We develop a general framework for weighted parsing which is built on top of grammar-based language models and employs flexible weight algebras. It generalizes previous work in that area (semiring parsing, weighted deductive parsing) and also covers applications outside the classical scope of parsing, e.g., algebraic dynamic programming. We show an algorithm which terminates and is correct for a large class of weighted grammar-based language models.},
author = {M{\"o}rbitz, Richard and Vogler, Heiko},
booktitle = {Proceedings of the 14th International Conference on Finite-State Methods and Natural Language Processing},
date-added = {2021-05-03 15:54:47 +0200},
date-modified = {2021-10-15 11:51:26 +0200},
pages = {46--55},
publisher = {Association for Computational Linguistics},
title = {Weighted parsing for grammar-based language models},
year = {2019},
bdsk-file-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxBpLi4vLi4vLi4vTGlicmFyeS9Nb2JpbGUgRG9jdW1lbnRzL2NvbX5hcHBsZX5DbG91ZERvY3MvQmlibGlvL0FydGljbGVzL01vcmJpdHpWb2dsZXIxOXdlaWdodGVkLXBhcnNpbmcucGRmTxEB/AAAAAAB/AACAAAHc3lzdGVtZQAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAEJEAAH/////H01vcmJpdHpWb2dsZXIxOXdlaSNGRkZGRkZGRi5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAP////8AAAAAAAAAAAAAAAAAAwAGAAAKIGN1AAAAAAAAAAAAAAAAAAhBcnRpY2xlcwACAHEvOlVzZXJzOmphY3F1ZW1hOkxpYnJhcnk6TW9iaWxlIERvY3VtZW50czpjb21+YXBwbGV+Q2xvdWREb2NzOkJpYmxpbzpBcnRpY2xlczpNb3JiaXR6Vm9nbGVyMTl3ZWlnaHRlZC1wYXJzaW5nLnBkZgAADgBIACMATQBvAHIAYgBpAHQAegBWAG8AZwBsAGUAcgAxADkAdwBlAGkAZwBoAHQAZQBkAC0AcABhAHIAcwBpAG4AZwAuAHAAZABmAA8AEAAHAHMAeQBzAHQAZQBtAGUAEgBvVXNlcnMvamFjcXVlbWEvTGlicmFyeS9Nb2JpbGUgRG9jdW1lbnRzL2NvbX5hcHBsZX5DbG91ZERvY3MvQmlibGlvL0FydGljbGVzL01vcmJpdHpWb2dsZXIxOXdlaWdodGVkLXBhcnNpbmcucGRmAAATAAEvAAAVAAIAD///AAAACAANABoAJACQAAAAAAAAAgEAAAAAAAAABQAAAAAAAAAAAAAAAAAAApA=},
bdsk-url-1 = {https://www.aclweb.org/anthology/W19-3108},
bdsk-url-2 = {https://doi.org/10.18653/v1/W19-3108}}
@inproceedings{Mohri15compression,
abstract = {We present a theoretical framework for the compression of automata, which are widely used representations in speech processing, natural language processing and many other tasks. As a corollary, our framework further covers graph compression. We introduce a probabilistic process of graph and automata generation that is similar to stationary ergodic processes and that covers real-world phenomena. We also introduce a universal compression scheme LZA for this probabilistic model and show that LZA significantly outperforms other compression techniques such as gzip and the UNIX compress command for several synthetic and real data sets.},
author = {Mohri, Mehryar and Riley, Michael and Suresh, Ananda Theertha},
booktitle = {2015 IEEE International Symposium on Information Theory (ISIT)},
date-added = {2021-05-01 19:27:17 +0200},
date-modified = {2021-05-01 19:28:24 +0200},
organization = {IEEE},
pages = {2989--2993},
title = {Automata and graph compression},
year = {2015},
bdsk-file-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxBcLi4vLi4vLi4vTGlicmFyeS9Nb2JpbGUgRG9jdW1lbnRzL2NvbX5hcHBsZX5DbG91ZERvY3MvQmlibGlvL0FydGljbGVzL01vaHJpMTVjb21wcmVzc2lvbi5wZGZPEQHGAAAAAAHGAAIAAAdzeXN0ZW1lAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAQkQAAf////8WTW9ocmkxNWNvbXByZXNzaW9uLnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA/////wAAAAAAAAAAAAAAAAADAAYAAAogY3UAAAAAAAAAAAAAAAAACEFydGljbGVzAAIAZC86VXNlcnM6amFjcXVlbWE6TGlicmFyeTpNb2JpbGUgRG9jdW1lbnRzOmNvbX5hcHBsZX5DbG91ZERvY3M6QmlibGlvOkFydGljbGVzOk1vaHJpMTVjb21wcmVzc2lvbi5wZGYADgAuABYATQBvAGgAcgBpADEANQBjAG8AbQBwAHIAZQBzAHMAaQBvAG4ALgBwAGQAZgAPABAABwBzAHkAcwB0AGUAbQBlABIAYlVzZXJzL2phY3F1ZW1hL0xpYnJhcnkvTW9iaWxlIERvY3VtZW50cy9jb21+YXBwbGV+Q2xvdWREb2NzL0JpYmxpby9BcnRpY2xlcy9Nb2hyaTE1Y29tcHJlc3Npb24ucGRmABMAAS8AABUAAgAP//8AAAAIAA0AGgAkAIMAAAAAAAACAQAAAAAAAAAFAAAAAAAAAAAAAAAAAAACTQ==}}
@article{Mohri09music,
abstract = {We present an approach to music identification based on weighted finite-state transducers and Gaussian mixture models, inspired by techniques used in large-vocabulary speech recognition. Our modeling approach is based on learning a set of elementary music sounds in a fully unsupervised manner. While the space of possible music sound sequences is very large, our method enables the construction of a compact and efficient representation for the song collection using finite-state transducers. This paper gives a novel and substantially faster algorithm for the construction of factor transducers, the key representation of song snippets supporting our music identification technique. The complexity of our algorithm is linear with respect to the size of the suffix automaton constructed. Our experiments further show that it helps speed up the construction of the weighted suffix automaton in our task by a factor of 17 with respect to our previous method using the intermediate steps of determinization and minimization. We show that, using these techniques, a large-scale music identification system can be constructed for a database of over 15 000 songs while achieving an identification accuracy of 99.4% on undistorted test data, and performing robustly in the presence of noise and distortions.},
author = {Mohri, Mehryar and Moreno, Pedro J and Weinstein, Eugene},
date-added = {2021-05-01 19:25:02 +0200},
date-modified = {2021-05-01 19:25:38 +0200},
journal = {IEEE transactions on audio, speech, and language processing},
number = {1},
pages = {197--207},
publisher = {IEEE},
title = {Efficient and robust music identification with weighted finite-state transducers},
volume = {18},
year = {2009},
bdsk-file-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxBWLi4vLi4vLi4vTGlicmFyeS9Nb2JpbGUgRG9jdW1lbnRzL2NvbX5hcHBsZX5DbG91ZERvY3MvQmlibGlvL0FydGljbGVzL01vaHJpMDl0YXNscC5wZGZPEQGuAAAAAAGuAAIAAAdzeXN0ZW1lAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAQkQAAf////8QTW9ocmkwOXRhc2xwLnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA/////wAAAAAAAAAAAAAAAAADAAYAAAogY3UAAAAAAAAAAAAAAAAACEFydGljbGVzAAIAXi86VXNlcnM6amFjcXVlbWE6TGlicmFyeTpNb2JpbGUgRG9jdW1lbnRzOmNvbX5hcHBsZX5DbG91ZERvY3M6QmlibGlvOkFydGljbGVzOk1vaHJpMDl0YXNscC5wZGYADgAiABAATQBvAGgAcgBpADAAOQB0AGEAcwBsAHAALgBwAGQAZgAPABAABwBzAHkAcwB0AGUAbQBlABIAXFVzZXJzL2phY3F1ZW1hL0xpYnJhcnkvTW9iaWxlIERvY3VtZW50cy9jb21+YXBwbGV+Q2xvdWREb2NzL0JpYmxpby9BcnRpY2xlcy9Nb2hyaTA5dGFzbHAucGRmABMAAS8AABUAAgAP//8AAAAIAA0AGgAkAH0AAAAAAAACAQAAAAAAAAAFAAAAAAAAAAAAAAAAAAACLw==}}
@inproceedings{dAntoni19symbolicRA,
abstract = {Symbolic Finite Automata and Register Automata are two orthogonal extensions of finite automata motivated by real-world problems where data may have unbounded domains. These automata address a demand for a model over large or infinite alphabets, respectively. Both automata models have interesting applications and have been successful in their own right. In this paper, we introduce Symbolic Register Au- tomata, a new model that combines features from both symbolic and register automata, with a view on applications that were previously out of reach. We study their properties and provide algorithms for emptiness, inclusion and equivalence checking, together with experimental results.},
author = {D'Antoni, Loris and Ferreira, Tiago and Sammartino, Matteo and Silva, Alexandra},
booktitle = {International Conference on Computer Aided Verification},
date-added = {2021-05-01 19:14:05 +0200},
date-modified = {2021-05-01 19:14:36 +0200},
organization = {Springer},
pages = {3--21},
title = {Symbolic register automata},
year = {2019},
bdsk-file-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxBdLi4vLi4vLi4vTGlicmFyeS9Nb2JpbGUgRG9jdW1lbnRzL2NvbX5hcHBsZX5DbG91ZERvY3MvQmlibGlvL0FydGljbGVzL2RBbnRvbmkxOXN5bWJvbGljUkEucGRmTxEBzAAAAAABzAACAAAHc3lzdGVtZQAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAEJEAAH/////F2RBbnRvbmkxOXN5bWJvbGljUkEucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAP////8AAAAAAAAAAAAAAAAAAwAGAAAKIGN1AAAAAAAAAAAAAAAAAAhBcnRpY2xlcwACAGUvOlVzZXJzOmphY3F1ZW1hOkxpYnJhcnk6TW9iaWxlIERvY3VtZW50czpjb21+YXBwbGV+Q2xvdWREb2NzOkJpYmxpbzpBcnRpY2xlczpkQW50b25pMTlzeW1ib2xpY1JBLnBkZgAADgAwABcAZABBAG4AdABvAG4AaQAxADkAcwB5AG0AYgBvAGwAaQBjAFIAQQAuAHAAZABmAA8AEAAHAHMAeQBzAHQAZQBtAGUAEgBjVXNlcnMvamFjcXVlbWEvTGlicmFyeS9Nb2JpbGUgRG9jdW1lbnRzL2NvbX5hcHBsZX5DbG91ZERvY3MvQmlibGlvL0FydGljbGVzL2RBbnRvbmkxOXN5bWJvbGljUkEucGRmAAATAAEvAAAVAAIAD///AAAACAANABoAJACEAAAAAAAAAgEAAAAAAAAABQAAAAAAAAAAAAAAAAAAAlQ=}}
@article{dAntoni17MSOFS,
abstract = {We extend the weak monadic second-order logic of one successor for finite strings (M2L-STR) to symbolic alphabets by allowing character predicates to range over decidable quantifier free theories instead of finite alphabets. We call this logic, which is able to describe sequences over complex and potentially infinite domains, symbolic M2L-STR (S-M2L-STR).
We present a decision procedure for S-M2L-STR based on a reduction to symbolic finite automata, a decidable extension of finite automata that allows transitions to carry predicates and can therefore model complex alphabets. The reduction constructs a symbolic automaton over an alphabet consisting of pairs of symbols where the first element of each pair is a symbol in the original formula's alphabet, while the second element is a bit-vector. To handle this modified alphabet we show that the Cartesian product of two decidable Boolean algebras, e.g., the product of formula's algebra and bit-vector's algebra, also forms a decidable Boolean algebra. T
o make the decision procedure practical, we propose two efficient representations of the Cartesian product of two Boolean algebras, one based on algebraic decision dia- grams and one on a variant of Shannon expansions.
Finally, we implement our decision procedure and evaluate it on more than 10,000 formulas. Despite the generality, our implementation has comparable performance with the state-of-the-art M2L-STR solvers.},
author = {D'Antoni, Loris and Veanes, Margus},
date-added = {2021-05-01 19:07:37 +0200},
date-modified = {2021-05-04 10:20:20 +0200},
journal = {ACM SIGPLAN Notices},
number = {1},
pages = {232--245},
publisher = {ACM New York, NY, USA},
title = {Monadic second-order logic on finite sequences},
volume = {52},