We consider the monadic second order logic with two suc- cessor functions and equality, interpreted on the binary tree. We show that a set of assignments is definable in the fragment ∑2 of this logic if and only if it is definable by a Büchi automaton. Moreover we show that every set of second order assignments definable in ∑2 with equality is definable in ∑2 without equality as well. The present paper is sketchy due to space constraints; for more details and proofs see [7].
A new logical characterization of B"uchi automata
LENZI, Giacomo
2001
Abstract
We consider the monadic second order logic with two suc- cessor functions and equality, interpreted on the binary tree. We show that a set of assignments is definable in the fragment ∑2 of this logic if and only if it is definable by a Büchi automaton. Moreover we show that every set of second order assignments definable in ∑2 with equality is definable in ∑2 without equality as well. The present paper is sketchy due to space constraints; for more details and proofs see [7].File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
