Monadic second-order logic, graph coverings and unfoldings of transition systems

doi:10.1016/S0168-0072(97)00048-1

Annals of Pure and Applied Logic

Volume 92, Issue 1, 11 March 1998, Pages 35-62

https://doi.org/10.1016/S0168-0072(97)00048-1 Get rights and content

Under an Elsevier user license

open archive

Abstract

We prove that every monadic second-order property of the unfolding of a transition system is a monadic second-order property of the system itself. An unfolding is an instance of the general notion of graph covering. We consider two more instances of this notion. A similar result is possible for one of them but not for the other.

Keywords

Second-order logic

Rabin automaton

Infinite tree

Semantics

Transition Systems

Graph covering

MSC

68Q55

MSC

03C80

03C85

Cited by (0)

¹: Partially supported by Polish KBN grant No. 2 P301 009 06. Part of this work was done at Basic Research in Computer Science, Centre of the Danish National Research Foundation.