Logic and rational languages of scattered and countable series-parallel posets (Q5919278)

From MaRDI portal
scientific article; zbMATH DE number 7159827
Language Label Description Also known as
English
Logic and rational languages of scattered and countable series-parallel posets
scientific article; zbMATH DE number 7159827

    Statements

    Logic and rational languages of scattered and countable series-parallel posets (English)
    0 references
    0 references
    0 references
    4 December 2019
    0 references
    29 January 2020
    0 references
    automata and logic
    0 references
    transfinite N-free posets
    0 references
    series-parallel posets
    0 references
    series-parallel rational languages
    0 references
    branching automata
    0 references
    monadic second-order logic
    0 references
    Presburger arithmetic
    0 references
    This paper gives a characterization in terms of logical expressions for some specific partial order indexed rational languages. More precisely, the authors consider N-free posets, which are models of concurrent programs equivalent to the series-parallel digraphs of [\textit{J. Valdes} et al., SIAM J. Comput. 11, 298--313 (1982; Zbl 0478.68065)]. Generalizing the notion of finite word, the paper considers mappings from countable N-free posets, whose chains are scattered (i.e. have no dense sub-ordering) and whose antichain are finite, into finite alphabets. In this setting, the notion of rational language introduced in [\textit{N. Bedon} and \textit{C. Rispal}, Theor. Comput. Sci. 412, No. 22, 2356--2369 (2011; Zbl 1238.68072)] is shown to be equivalent to definability in the logic P-MSO of [\textit{N. Bedon}, Log. Methods Comput. Sci. 11, No. 4, Paper No. 2, 38 p. (2015; Zbl 1448.68255)]. P-MSO combines monadic second-order logic with Presburger arithmetic, which is the theory of natural numbers under addition. Since the transformation from P-MSO to rational expressions follows well-known techniques, the paper focus on the converse transformation. The proof proceeds by first constructing, from a rational expression, a more specific one called a \(>1\)-expression, and from this \(>1\)-expression a graph, called a \(D\)-graph, before constructing the final P-MSO formula. The paper is the extended version, with proofs, of [the authors, Lect. Notes Comput. Sci. 11417, 275--287 (2019; Zbl 1425.03013)].
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references

    Identifiers

    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references