225:
and structural induction over the definition of ω-regular language, it can be easily shown that a Büchi automaton can be constructed for any given ω-regular language.
136:
It is a straightforward consequence of the definition that the ω-regular languages are precisely the ω-languages of the form
221:: Every ω-regular language is recognized by a nondeterministic Büchi automaton; the translation is constructive. Using the
478:
occurs infinitely often in the accepting run. Let's pick the strictly increasing infinite sequence of indexes
841:
222:
874:
837:
247:, we construct an ω-regular language and then we will show that this language is recognized by
16:
Class of ω-languages that generalize the definition of regular languages to infinite words
8:
840:
showed in 1962 that ω-regular languages are precisely the ones definable in a particular
211:
327:
28:
854:
859:
Handbook of
Theoretical Computer Science, volume B: Formal Models and Semantics
24:
868:
122:
97:
are ω-regular languages (this rule can only be applied finitely many times)
133:, which is not an ω-language and therefore not an ω-regular language.
656:
Therefore, there is an infinite and strictly increasing sequence
861:, pages 133-192. Elsevier Science Publishers, Amsterdam, 1990.
832:
121:
could be for example {ε}, the set containing only the
57:
is a regular language not containing the empty string
853:
Wolfgang Thomas, "Automata on infinite objects." In
200:
866:
801:). By this construction, there is a run of
214:if and only if it is an ω-regular language.
105:are obtained by concatenating words from
63:, the concatenation of a regular language
833:Equivalence to Monadic second-order logic
336:that is accepted by the finite automaton
228:Conversely, for a given Büchi automaton
867:
223:closure properties of Büchi automata
117:is not necessarily ω-regular, since
109:infinitely many times. Note that if
37:
197:s do not contain the empty string.
13:
363:We claim that the Büchi automaton
27:that generalize the definition of
14:
886:
210:An ω-language is recognized by a
813:occurs infinitely often. Hence,
188:s are regular languages and the
46:is ω-regular if it has the form
847:
201:Equivalence to Büchi automaton
1:
768:≥0, there is a finite run of
447:,... is an accepting run of
7:
741:, there is a finite run of
10:
891:
842:monadic second-order logic
466:and there must be a state
67:and an ω-regular language
367:recognizes the language
280:) be the finite segment
499:... such that, for all
805:, which starts from
610:Conversely, suppose
411:Let's suppose word
31:to infinite words.
21:ω-regular languages
734:By definition of
38:Formal definition
29:regular languages
882:
875:Formal languages
827:
812:
808:
779:
775:
771:
752:
748:
744:
733:
696:
655:
644:
634:
607:
582:
545:
516:
512:
477:
469:
465:
425:
405:
355:
328:regular language
325:
251:. For an ω-word
246:
125:, in which case
101:The elements of
890:
889:
885:
884:
883:
881:
880:
879:
865:
864:
855:Jan van Leeuwen
850:
835:
814:
810:
806:
800:
789:
777:
773:
769:
763:
750:
746:
742:
739:
730:
724:
714:
698:
694:
688:
678:
676:
669:
662:
646:
636:
627:
620:
611:
604:
597:
595:
584:
579:
573:
563:
547:
544:
543:
539:
528:
518:
514:
511:
510:
504:
498:
491:
484:
475:
467:
463:
461:
446:
439:
432:
412:
398:
391:
386:
368:
353:
337:
334:
320:
313:
307:
299:
289:
267:
261:
229:
212:Büchi automaton
203:
196:
187:
178:
165:
157:
148:
142:
40:
34:
23:are a class of
17:
12:
11:
5:
888:
878:
877:
863:
862:
849:
846:
834:
831:
830:
829:
795:
787:
761:
737:
728:
719:
710:
692:
686:
677:... such that
674:
667:
660:
625:
618:
608:
602:
593:
591:
577:
568:
559:
541:
537:
533:
526:
508:
506:
496:
489:
482:
459:
444:
437:
430:
406:
396:
389:
370:
351:
332:
326:, we define a
318:
303:
294:
284:
265:
259:
202:
199:
192:
183:
174:
161:
153:
146:
140:
99:
98:
80:
58:
42:An ω-language
39:
36:
15:
9:
6:
4:
3:
2:
887:
876:
873:
872:
870:
860:
856:
852:
851:
845:
843:
839:
825:
821:
817:
809:and in which
804:
798:
794:
790:
783:
767:
760:
756:
740:
731:
722:
718:
713:
709:
705:
701:
697:and, for all
695:
685:
681:
673:
666:
659:
653:
649:
643:
639:
632:
628:
621:
614:
609:
605:
598:
587:
580:
571:
567:
562:
558:
554:
550:
546:and, for all
536:
532:
525:
521:
517:. Therefore,
502:
495:
488:
481:
473:
458:
455:. Therefore,
454:
450:
443:
436:
429:
423:
419:
415:
410:
407:
403:
399:
392:
385:
381:
377:
373:
366:
362:
359:
358:
357:
349:
345:
341:
335:
329:
324:
316:
311:
306:
302:
297:
293:
287:
283:
279:
275:
271:
264:
258:
254:
250:
244:
240:
236:
232:
226:
224:
220:
216:
215:
213:
207:
198:
195:
191:
186:
182:
177:
173:
169:
164:
160:
156:
152:
145:
139:
134:
132:
128:
124:
120:
116:
112:
108:
104:
96:
92:
88:
84:
81:
79:well-defined)
78:
74:
70:
66:
62:
59:
56:
52:
49:
48:
47:
45:
35:
32:
30:
26:
22:
858:
848:Bibliography
844:called S1S.
836:
823:
819:
815:
802:
796:
792:
785:
781:
765:
758:
754:
735:
726:
720:
716:
711:
707:
703:
699:
690:
683:
679:
671:
664:
657:
651:
647:
641:
637:
630:
623:
616:
612:
600:
589:
585:
575:
569:
565:
560:
556:
552:
548:
534:
530:
523:
519:
500:
493:
486:
479:
471:
456:
452:
448:
441:
434:
427:
421:
417:
413:
408:
401:
394:
387:
383:
379:
375:
371:
364:
360:
347:
343:
339:
330:
322:
314:
312:. For every
309:
304:
300:
295:
291:
285:
281:
277:
273:
269:
262:
256:
252:
248:
242:
238:
234:
230:
227:
218:
217:
209:
205:
204:
193:
189:
184:
180:
175:
171:
170:, where the
167:
162:
158:
154:
150:
143:
137:
135:
130:
126:
123:empty string
118:
114:
113:is regular,
110:
106:
102:
100:
94:
90:
86:
82:
76:
72:
68:
64:
60:
54:
50:
43:
41:
33:
20:
18:
764:). For all
583:Therefore,
71:(Note that
25:ω-languages
857:, editor,
474:such that
635:for some
629:− {
400:− {
166:for some
869:Category
780:on word
753:on word
268:... let
237:, Σ, δ,
149:∪ ... ∪
206:Theorem
179:s and
462:is in
409:Proof:
361:Lemma:
89:where
53:where
838:Büchi
772:from
745:from
729:q',q'
626:q',q'
603:q',q'
578:q',q'
397:q',q'
342:, Σ,
219:Proof
738:q,q'
702:≥0,
693:q,q'
689:) ∈
645:and
619:q,q'
551:≥0,
503:≥0,
426:and
404:} ).
390:q,q'
333:q,q'
93:and
19:The
776:to
757:(0,
749:to
682:(0,
633:} )
596:,q'
522:(0,
513:is
470:in
451:on
356:.
350:, {
308:of
290:...
233:= (
77:not
75:is
871::
818:∈
811:q'
799:+1
778:q'
774:q'
751:q'
725:)∈
723:+1
650:'∈
615:∈
606:).
588:∈
574:)∈
572:+1
542:q'
529:)∈
515:q'
476:q'
468:q'
416:∈
382:'∈
354:})
352:q'
346:,
321:∈
319:q'
317:,
298:-1
288:+1
255:=
241:,
85:∪
73:BA
61:AB
828:.
826:)
824:A
822:(
820:L
816:w
807:q
803:A
797:k
793:i
791:,
788:k
786:i
784:(
782:w
770:A
766:k
762:0
759:i
755:w
747:q
743:A
736:L
732:.
727:L
721:k
717:i
715:,
712:k
708:i
706:(
704:w
700:k
691:L
687:0
684:i
680:w
675:2
672:i
670:,
668:1
665:i
663:,
661:0
658:i
654:.
652:F
648:q
642:I
640:∈
638:q
631:ε
624:L
622:(
617:L
613:w
601:L
599:(
594:0
592:q
590:L
586:w
581:.
576:L
570:k
566:i
564:,
561:k
557:i
555:(
553:w
549:k
540:,
538:0
535:q
531:L
527:0
524:i
520:w
509:k
507:i
505:q
501:k
497:2
494:i
492:,
490:1
487:i
485:,
483:0
480:i
472:F
464:I
460:0
457:q
453:w
449:A
445:2
442:q
440:,
438:1
435:q
433:,
431:0
428:q
424:)
422:A
420:(
418:L
414:w
402:ε
395:L
393:(
388:L
384:F
380:q
378:,
376:I
374:∈
372:q
369:⋃
365:A
348:q
344:δ
340:Q
338:(
331:L
323:Q
315:q
310:w
305:j
301:a
296:j
292:a
286:i
282:a
278:j
276:,
274:i
272:(
270:w
266:2
263:a
260:1
257:a
253:w
249:A
245:)
243:F
239:I
235:Q
231:A
208::
194:i
190:B
185:i
181:B
176:i
172:A
168:n
163:n
159:B
155:n
151:A
147:1
144:B
141:1
138:A
131:A
129:=
127:A
119:A
115:A
111:A
107:A
103:A
95:B
91:A
87:B
83:A
69:B
65:A
55:A
51:A
44:L
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.