Monadic second-order logic, graph coverings and unfoldings of transition systems
type: Item
instance of: scholarly article
title: Monadic second-order logic, graph coverings and unfoldings of transition systems
zbMATH Open document ID: 0929.03036
DOI: 10.1016/S0168-0072(97)00048-1
author: Igor Walukiewicz
author: Bruno Courcelle
published in: Annals of Pure and Applied Logic
publication date: 1999-11-03T00:00:00Z
review text: Transition systems are directed graphs which can be regarded as abstract programs and then their unfoldings represent the behaviours of programs. When transition systems are defined as relational structures, monadic second-order (MSO) logic offers a natural formalism for expressing their properties. In an earlier paper, the first author conjectured that if the unfoldings of the transition systems of a class \(P\) are definable by an MSO formula, then \(P\) itself is also effectively MSO-definable. Here, the conjecture is proved for transition systems with countable outdegrees. The tools used in the proof include automata on infinite trees and coverings of transition systems. Such coverings, which are homomorphisms of graphs, are extensively studied from various points of view and they are also considered in the context of general directed graphs.
Mathematics Subject Classification ID: 03B70
Mathematics Subject Classification ID: 68Q55
Mathematics Subject Classification ID: 05C20
Mathematics Subject Classification ID: 03C85
Mathematics Subject Classification ID: 03D05
Mathematics Subject Classification ID: 68Q45
Mathematics Subject Classification ID: 03B15
zbMATH DE Number: 1308058
zbMATH Keywords: monadic second-order logic
zbMATH Keywords: transition systems
zbMATH Keywords: relational structures
zbMATH Keywords: unfoldings
zbMATH Keywords: automata on infinite trees
zbMATH Keywords: coverings of transition systems
zbMATH Keywords: directed graphs
reviewed by: Magnus Steinby
MaRDI profile type: Publication
cites work: Q3852212
cites work: Monadic second-order definable graph transductions: a survey
cites work: Erratum to ``The monadic second-order logic of graphs. VI: On several representations of graphs by relational structures''
cites work: The monadic second-order logic of graphs. IX: Machines and their behaviours
cites work: Q3753490
cites work: Alternating automata with start formulas
cites work: Decidability of Second-Order Theories and Automata on Infinite Trees
cites work: Q3346281
cites work: The monadic theory of order
cites work: Q4714446
cites work: Monadic second order logic on tree-like structures
full work available at URL: s0168-0072(97)00048-1
OpenAlex ID: W2067672151
Recommended article: Q3975133
Recommended article: Monadic second-order definable graph transductions: a survey
Recommended article: Q3077955
Recommended article: Q4218947
Recommended article: Q2767003
Recommended article: Monadic Second-Order Logic and Transitive Closure Logics over Trees
Recommended article: Q4362731
Recommended article: Graph Structure and Monadic Second-Order Logic: Language Theoretical Aspects
description: scientific article; zbMATH DE number 1308058