Toto je starší verze dokumentu!
—-
pozice | |
unární predikát značící, že na pozici je písmeno a |
|
pozice je před | |
logické spojky | |
kvantifikace | |
+ rovnost |
pozice | |
unární predikát značící, že na pozici je písmeno a |
|
pozice je před | |
logické spojky | |
kvantifikace | |
množiny pozic | |
leží v | |
kvantifikace nad množinami pozic |
Proměnné ve formuli mohou být:
Sentence
Valuace přiřazuje hodnotu volným proměnným.
NFA → sentence MSO t.ž.
máme množinu pozic odpovídající stavům původního automatu | |
každá pozice odpovídá některému stavu | |
každá pozice neodpovídá dvěma různým stavům | |
první prvek odpovídá počátečnímu stavu | |
definice přechodů | |
poslední prvek odpovídá finálnímu stavu | |
First, Succ, Last jsou jednoduše definovatelná makra