A DECISION PROCEDURE FOR THE MONADIC 2ND- ORDER LOGIC OF ONE SUCCESSOR

Authors
CALBRIX H NIVAT M PODELSKI A
Citation
H. Calbrix et al., A DECISION PROCEDURE FOR THE MONADIC 2ND- ORDER LOGIC OF ONE SUCCESSOR, Comptes rendus de l'Academie des sciences. Serie 1, Mathematique, 318(9), 1994, pp. 847-850
Citations number
6
Categorie Soggetti
Mathematics, General",Mathematics
Journal title
Comptes rendus de l'Academie des sciences. Serie 1, Mathematique → ACNP
ISSN journal
07644442
Volume
318
Issue
9
Year of publication
1994
Pages
847 - 850
Database
ISI
SICI code
0764-4442(1994)318:9<847:ADPFTM>2.0.ZU;2-1
Abstract
Since they have been introduced by Richard Bachi in 1962, Bachi automa ta recognizing sets of infinite words are basic tools of decisions pro ofs of the monadic logic SIS and temporal logics, used in program and circuit checking. We are showing in this Note that we can get rid of a utomata on infinite words thanks to a finite representation of infinit e ultimately periodic words recognized by a Bachi automaton. Moreover, our procedure produces minimal deterministic automata.