Order-Invariant MSO is Stronger than Counting MSO in the Finite

Tobias Ganzow; Sasha Rubin

Home/Archive/arXiv

arXiv · 0706.3723

Order-Invariant MSO is Stronger than Counting MSO in the Finite

Tobias Ganzow·Sasha Rubin

View original source ↗Read source document ↗Export metadata ↓

Abstract

We compare the expressiveness of two extensions of monadic second-order logic (MSO) over the class of finite structures. The first, counting monadic second-order logic (CMSO), extends MSO with first-order modulo-counting quantifiers, allowing the expression of queries like ``the number of elements in the structure is even''. The second extension allows the use of an additional binary predicate, not contained in the signature of the queried structure, that must be interpreted as an arbitrary linear order on its universe, obtaining order-invariant MSO. While it is straightforward that every CMSO formula can be translated into an equivalent order-invariant MSO formula, the converse had not yet been settled. Courcelle showed that for restricted classes of structures both order-invariant MSO and CMSO are equally expressive, but conjectured that, in general, order-invariant MSO is stronger than CMSO. We affirm this conjecture by presenting a class of structures that is order-invariantly definable in MSO but not definable in CMSO.

Explore related subjects

cs.LO

Keep this discovery

Explore connections, maps & timelines

BibTeX RIS

Tobias Ganzow, Sasha Rubin. 2008-03-20. Order-Invariant MSO is Stronger than Counting MSO in the Finite. https://arxiv.org/abs/0706.3723

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Overview and Roadmap of Team Automata

Team Automata is a formalism for interacting component-based systems proposed in 1997, whereby multiple sending and receiving actions from concurrent automata can synchronise. During the past 25+ years, team automata have been studied and applied in many different contexts, involving 25+ researchers and resulting in 25+ publications. In this paper, we first revisit the specific notion of synchronisation and composition of team automata, relating it to other relevant coordination models, such as Reo, BIP, Contract Automata, Choreography Automata, and Multi-Party Session Types. We then identify several aspects that have recently been investigated for team automata and related models. These include communication properties (which are the properties of interest?), realisability (how to decompose a global model into local components?), tool support (what has been automatised or implemented?), and variability (can a family of concrete product (automata) models be captured concisely?). Our presentation of these aspects provides a snapshot of the most recent trends in research on team automata, and delineates a roadmap for future research, both for team automata and for related formalisms.

cs.LO↗

arXiv2026

Derivatives for Containers in Univalent Foundations

Containers conveniently represent a wide class of inductive data types. Their derivatives compute representations of types of one-hole contexts, useful for implementing tree-traversal algorithms. Derivatives of discrete containers (whose positions have decidable equality) satisfy a universal property with respect to linear morphisms of containers. This induces a well-behaved notion of linear substitution for one-hole contexts. Working in Univalent Foundations, we extend the derivative operation to untruncated containers (whose shapes and positions are arbitrary types). We prove that this derivative, defined in terms of a set of isolated positions, satisfies an appropriate universal property in the wild category of untruncated containers and linear morphisms, as well as basic laws with respect to constants, sums and products. A chain rule exists, but is in general non-invertible. In fact, a globally invertible chain rule is inconsistent in the presence of non-set types, and equivalent to a classical principle when restricted to set-truncated containers. We derive a rule for derivatives of least fixpoints from the chain rule, and characterize its invertibility. All of our results are formalized in Cubical Agda.

cs.LO↗

arXiv2026

Model Checking HyperRecHML is Decidable

Temporal hyperlogics combine explicit quantification over traces with temporal requirements evaluated over the quantified traces. HyperRecHML is a temporal hyperlogic which allows for arbitrary mixing of trace quantification and the use of fixed points for expressing temporal requirements, which makes it very expressive in comparison to other first-order hyperlogics. HyperRecHML has already been successfully applied in runtime verification, but the decidability of its model checking problem remains open. We answer this question positively by providing two main contributions. Firstly, a normalization procedure that allows to reduce arbitrary HyperRecHML formulas to a normal form with restricted nesting of trace quantification and fixed points. Secondly, we provide an automata-based model checking algorithm for formulas of this normal form. The complexity of our algorithm is comparable to similar ones for other hyperlogics, despite the extra expressive power.

cs.LO↗