We study the conditions under which monadic second-order (MSO) interpretations can be simplified by replacing representations of elements as tuples of arbitrary sets with representations as tuples of finite sets or points. Using reparameterizations of MSO formulas, we prove that for formulas with free finite-set variables, it is decidable whether a point reparameterization exists, and that such a reparameterization can be effectively constructed over countable chains. Moreover, over countable Dedekind-complete labeled chains, a formula with free arbitrary set variables admits a finite-set reparameterization if and only if it has at most countably many satisfying assignments. These results yield effective simplification procedures for MSO interpretations over broad classes of countable linear orders.

We study the uniformisation problem for monadic second-order logic (MSO) over countable ordinal chains. Given a formula defining a relation between subsets of the input structure, the question is whether there exists a formula that defines a function selecting, for every set in the domain of the relation, a unique set such that the pair belongs to the relation. It is known, due to Lifsches and Shelah [Lifsches and Shelah, 1998], that MSO cannot, in general, be uniformised over the class of countable ordinals. We show that the maximal uniformisation degree is reached by extending the logic with a predicate that, given a set, selects (when possible) a cofinal subset of order type ω. Equivalently, every MSO formula can be uniformised over the class of countable ordinal chains using a formula in this extended logic.

In this work, we consider two extensions of monadic second-order logic, and study in what cases the classical decidability results are preserved. The first extension, MSO[CBrank_β], is MSO (over the signature of the binary tree) augmented with the extra ability to express that the subtree over a set X has Cantor-Bendixson rank β, for some fixed countable ordinal β. We show that this extension is decidable over the binary tree if and only if β is finite, which means that it is decidable if and only if it is equivalent in expressiveness to MSO. The second extension, MSO[otp_α], is MSO (over the signature of order) augmented with the extra ability to express that the suborder induced by a set X has order type α for some fixed countable ordinal α. We show that this extension is decidable over countable ordinals if and only if α < ω^ω, which means that it is decidable if and only if it is equivalent in expressiveness to MSO. The first result can be established as a consequence of the second. The second result relies on the undecidability results of the logic BMSO (itself relying on the undecidability of MSO+U) in the case of ω^β for β a limit ordinal, and on entirely new techniques when β is a successor ordinal. We also have some partial extensions of the second result to some uncountable cases.

The Church Problem asks for the construction of a procedure which, given a logical specification A(I,O) between input omega-strings I and output omega-strings O, determines whether there exists an operator F that implements the specification in the sense that A(I, F(I)) holds for all inputs I. Buchi and Landweber provided a procedure to solve the Church problem for MSO specifications and operators computable by finite-state automata. We investigate a generalization of the Church synthesis problem to the continuous time domain of the non-negative reals. We show that in the continuous time domain there are phenomena which are very different from the canonical discrete time domain of the natural numbers.

An automaton is unambiguous if for every input it has at most one accepting computation. An automaton is finitely (respectively, countably) ambiguous if for every input it has at most finitely (respectively, countably) many accepting computations. An automaton is boundedly ambiguous if there is k ∈ ℕ, such that for every input it has at most k accepting computations. We consider Parity Tree Automata (PTA) and prove that the problem whether a PTA is not unambiguous (respectively, is not boundedly ambiguous, not finitely ambiguous) is co-NP complete, and the problem whether a PTA is not countably ambiguous is co-NP hard.

An automaton is unambiguous if for every input it has at most one accepting computation. An automaton is finitely (respectively, countably) ambiguous if for every input it has at most finitely (respectively, countably) many accepting computations. An automaton is boundedly ambiguous if there is k in N, such that for every input it has at most k accepting computations. We consider nondeterministic Büchi automata (NBA) over infinite trees and prove that it is decidable in polynomial time, whether an automaton is unambiguous, boundedly ambiguous, finitely ambiguous, or countably ambiguous.

An automaton is unambiguous if for every input it has at most one accepting computation. An automaton is k-ambiguous (for k > 0) if for every input it has at most k accepting computations. An automaton is boundedly ambiguous if it is k-ambiguous for some $k \in \mathbb{N}$. An automaton is finitely (respectively, countably) ambiguous if for every input it has at most finitely (respectively, countably) many accepting computations. The degree of ambiguity of a regular language is defined in a natural way. A language is k-ambiguous (respectively, boundedly, finitely, countably ambiguous) if it is accepted by a k-ambiguous (respectively, boundedly, finitely, countably ambiguous) automaton. Over finite words every regular language is accepted by a deterministic automaton. Over finite trees every regular language is accepted by an unambiguous automaton. Over $\omega$-words every regular language is accepted by an unambiguous B\"uchi automaton and by a deterministic parity automaton. Over infinite trees Carayol et al. showed that there are ambiguous languages. We show that over infinite trees there is a hierarchy of degrees of ambiguity: For every k > 1 there are k-ambiguous languages that are not k - 1 ambiguous; and there are finitely (respectively countably, uncountably) ambiguous languages that are not boundedly (respectively finitely, countably) ambiguous.

We study the expressive power of logical interpretations on the class of scattered trees, namely those with countably many infinite branches. Scattered trees can be thought of as the tree analogue of scattered linear orders. Every scattered tree has an ordinal rank that reflects the structure of its infinite branches. We prove, roughly, that trees and orders of large rank cannot be interpreted in scattered trees of small rank. We consider a quite general notion of interpretation: each element of the interpreted structure is represented by a set of tuples of subsets of the interpreting tree. Our trees are countable, not necessarily finitely branching, and may have finitely many unary predicates as labellings. We also show how to replace injective set-interpretations in (not necessarily scattered) trees by âfinitary' set-interpretations.

Abstract Rationals and countable ordinals are important examples of structures with decidable monadic second-order theories. A chain is an expansion of a linear order by monadic predicates. We show that if the monadic second-order theory of a countable chain C is decidable then C has a non-trivial expansion with decidable monadic second-order theory.

Abstract We investigate the extension of monadic second-order logic of order with cardinality quantifiers “there exists uncountably many sets such that…” and “there exists continuum many sets such that … ”. We prove that over the class of countable linear orders the two quantifiers are equivalent and can be effectively and uniformly eliminated. Weaker or partial elimination results are obtained for certain wider classes of chains. In particular, we show that over the class of ordinals the uncountability quantifier can be effectively and uniformly eliminated. Our argument makes use of Shelah's composition method and Ramsey-like theorem for dense linear orders.

Alternating timed automata are a powerful extension of classical Alur-Dill timed automata that are closed under all Boolean operations. They have played a key role, among others, in providing verification algorithms for prominent specification formalisms such as Metric Temporal Logic. Unfortunately, when interpreted over an infinite dense time domain (such as the reals), alternating time automata have an undecidable language emptiness problem. The main result of this paper is that, over bounded time domains, language emptiness for alternating timed automata is decidable (but nonelementary). The proof involves showing decidability of a class of parametric McNaughton games that are played over timed words and that have winning conditions expressed in the monadic logic of order augmented with the distance-one relation. As a corollary, we establish the decidability of the time-bounded model-checking problem for Alur-Dill timed automata against specifications expressed as alternating timed automata.

We study an extension of monadic second-order logic of order with the uncountability quantifier "there exist uncountably many sets". We prove that, over the class of finitely branching trees, this extension is equally expressive to plain monadic second-order logic of order. Additionally we find that the continuum hypothesis holds for classes of sets definable in monadic second-order logic over finitely branching trees, which is notable for not all of these classes are analytic. Our approach is based on Shelah's composition method and uses basic results from descriptive set theory. The elimination result is constructive, yielding a decision procedure for the extended logic.

An infinite binaryword can be identified with a branch in the full binary tree. We consider sets of branches definable in monadic second-order logic over the tree, where we allow some extra monadic predicates on the nodes. We show that this class equals to the Boolean combinations of sets in the Borel class Σ $^0_2$ over the Cantor discontinuum. Note that the last coincides with the Borel complexity of ω-regular languages.

Abstract We show that for no chain C there is a monadic-second order interpretation of the full binary tree in C.

Church's Problem asks for the construction of a procedure which, given a logical specification $\varphi$ on sequence pairs, realizes for any input sequence $I$ an output sequence $O$ such that $(I,O)$ satisfies $\varphi$. McNaughton reduced Church's Problem to a problem about two-player$\omega$-games. B\"uchi and Landweber gave a solution for Monadic Second-Order Logic of Order ($\MLO$) specifications in terms of finite-state strategies. We consider two natural generalizations of the Church problem to countable ordinals: the first deals with finite-state strategies; the second deals with $\MLO$-definable strategies. We investigate games of arbitrary countable length and prove the computability of these generalizations of Church's problem.

Abstract A monadic formula ψ(Y) is a selector for a formula φ(Y) in a structure if there exists a unique subset P of which satisfies ψ and this P also satisfies φ. We show that for every ordinal α ≥ ωω there are formulas having no selector in the structure (α, <). For α ≤ ω1, we decide which formulas have a selector in (α, <) , and construct selectors for them. We deduce the impossibility of a full generalization of the Büchi-Landweber solvability theorem from (ω, <) to (ωω, <). We state a partial extension of that theorem to all countable ordinals. To each formula we assign a selection degree which measures “how difficult it is to select”. We show that in a countable ordinal all non-selectable formulas share the same degree.

We prove a conjecture by A. Pnueli and strengthen it showing a sequence of "counting modalities" none of which is expressible in the temporal logic generated by the previous modalities, over the real line, or over the positive reals. Moreover, there is no finite temporal logic that can express all of them over the real line, so that no finite metric temporal logic is expressively complete.

For a two-variable formula ψ(X,Y) of Monadic Logic of Order (MLO) the Church Synthesis Problem concerns the existence and construction of an operator Y=F(X) such that ψ(X,F(X)) is universally valid over Nat. B\"{u}chi and Landweber proved that the Church synthesis problem is decidable; moreover, they showed that if there is an operator F that solves the Church Synthesis Problem, then it can also be solved by an operator defined by a finite state automaton or equivalently by an MLO formula. We investigate a parameterized version of the Church synthesis problem. In this version ψ might contain as a parameter a unary predicate P. We show that the Church synthesis problem for P is computable if and only if the monadic theory of is decidable. We prove that the B\"{u}chi-Landweber theorem can be extended only to ultimately periodic parameters. However, the MLO-definability part of the B\"{u}chi-Landweber theorem holds for the parameterized version of the Church synthesis problem.

The aim of this article is to examine the applicability of a compositional method developed for a generalized product construction by Feferman and Vaught to the field of program verification.We suggest an instance of the generalized product construction and prove an appropriate composition theorem for modal logic. We illustrate the usefulness of this generalized product by showing that many “parallel composition” operations are special cases of this generalized product.We obtain positive results (the compositional method works) for basic propositional modal logic, and negative results (the compositional method fails) for more expressive logics which can express EGp---“there is a path such that all the nodes of the path have the propertyp.”Applications of the composition theorem to the model-checking problem and to the parametric model-checking problem are provided.

A predicate logic of probability, close to the logics of probability of Halpern et al., is introduced. Our main result concerns the following model-checking problem: deciding whether a given formula holds on the structure defined by a given finite probabilistic process. We show that this model-checking problem is decidable for a rather large subclass of formulas of a second-order monadic logic of probability. We discuss also the decidability of satisfiability and compare our logic of probability with the probabilistic temporal logic pCTL*. * Partially supported by French-Israeli Arc-en-ciel/Keshet project No. 30 and No. 15.

A major result concerning Temporal Logics (T L) is Kamp's theorem which states that the temporal logic over the pair of modalities X until YandXsinceY is expressively complete for the first‐order fragment of monadic logic of order over the natural numbers. We show that there is no finite set of modalities B such that the temporal logic over B and monadic logic of order have the same expressive power over the natural numbers. As a consequence of our proof, we obtain that there is no finite base temporal logic which is expressively complete for the μ‐calculus.

The paper deals with logically definable families of sets (or point‐sets) of rational numbers. In particular we are interested whether the families definable over the real line with a unary predicate for the rationals are definable over the rational order alone. Let φ(X, Y) and ψ(Y) range over formulas in the first‐order monadic language of order. Let Q be the set of rationals and F be the family of subsets J of Q such that φ(Q, J) holds over the real line. The question arises whether, for every φ, F can be defined by means of an appropriate ψ(Y) interpreted over the rational order. We answer the question negatively. The answer remains negative if the first‐order logic is strengthened to weak monadic second‐order logic. The answer is positive for the restricted version of monadic second‐order logic where set quantifiers range over open sets. The case of full monadic second‐order logic remains open.

In [8, 11] the expressive completeness of the Propositional fragment of Duration Calculus relative to monadic first-order logic of order was established. In this paper we show that there is at least an exponential blow-up in every meaning preserving translation from monadic logic to PDC. Hence, there exists an exponential gap between the succinctness of monadic logic and that of duration calculus.

We consider the monadic second-order theory of linear order. For the sake of brevity, linearly ordered sets will be called chains. Let = ⟨A <⟩ be a chain. A formula ø(t) with one free individual variable t defines a point-set on A which contains the points of A that satisfy ø(t). As usually we identify a subset of A with its characteristic predicate and we will say that such a formula defines a predicate on A. A formula (X) one free monadic predicate variable defines the set of predicates (or family of point-sets) on A that satisfy (X). This family is said to be definable by (X) in A. Suppose that is a subchain of = ⟨B, <⟩. With a formula (X, A) we associate the following family of point-sets (or set of predicates) {P : P ⊆ A and (P, A) holds in } on A. This family is said to be definable by in with at the background. Note that in such a definition bound individual (respectively predicate) variables of range over B (respectively over subsets of B). Hence, it is reasonable to expect that the presence of a background chain allows one to define point sets (or families of point-sets) on A which are not definable inside .

We show that the expressive power of the branching time logic CTL coincides with that of the class of bisimulation invariant properties expressible in so-called monadic path logic: monadic second order logic in which set quantification is restricted to paths. In order to prove this result, we first prove a new composition theorem for trees. This approach is adapted from the approach of Hafer and Thomas in their proof that CTL coincides with the whole of monadic path logic over the class of full binary trees.

We consider an interpretation of monadic second-order logic of order in the continuous time structure of finitely variable signals and show the decidability of monadic logic in this structure. The expressive power of monadic logic is illustrated by providing a straightforward meaning preserving translation into monadic logic of three typical continuous time specification formalism: temporal logic of reals, restricted duration calculus and the propositional fragment of mean value calculus. As a by-product of the decidability of monadic logic we obtain that the above formalisms are decidable even when extended by quantifiers.

A Markovian technique is described to calculate the exact performance of the Viterbi algorithm used as either a channel decoder or a source encoder for a convolutional code. The probability of information bit error and the expected Hamming distortion are computed for codes of various rates and constraint lengths. The concept of tie-breaking rules is introduced and its influence on decoder performance is examined. Computer simulation is used to verify the accuracy of the results. Finally, we discuss the issue of when a coded system outperforms an uncoded system in light of the new results.>

The paper describes Markov methods for analyzing the expected and worst case performance of sequence-based methods of quantization. We suppose that the quantization algorithm is dynamic programming, where the current step depends on a vector of path metrics, which we call a metric function. Our principal objective is a concise representation of these metric functions and the possible trajectories of the dynamic programming algorithm. We shall consider quantization of equiprobable binary data using a convolutional code. Here the additive group of the code splits the set of metric functions into a finite collection of subsets. The subsets form the vertices of a directed graph, where edges are labeled by aggregate incremental increases in mean squared error (MSE). Paths in this graph correspond both to trajectories of the Viterbi algorithm and to cosets of the code. For the rate 1/2 convolutional code [1+D/sup 2/, 1+D+D/sup 2/], this graph has only nine vertices. In this case it is particularly simple to calculate per dimension expected and worst case MSE, and performance is slightly better than the binary [24, 12] Golay code. Our methods also apply to quantization of arbitrary symmetric probability distributions on [0, 1] using convolutional codes. For the uniform distribution on [0, 1], the expected MSE is the second moment of the "Voronoi region" of an infinite-dimensional lattice determined by the convolutional code. It may also be interpreted as an increase in the reliability of a transmission scheme obtained by nonequiprobable signaling. For certain convolutional codes we obtain a formula for expected MSE that depends only on the distribution of differences for a single pair of path metrics.>

The authors investigate and compare two ways of specifying stream relations (in particular, stream functions). The first uses relational programs, i.e., netlike program schemes in which the signature primitives are interpreted as relations over a given CPO. No stream domains are assumed; semantics is in fixed-point style. The second is through data flow nets, i.e., nets whose nodes are interpreted as processes (computational stations). The authors prove the existence of an adequate data flow interpreter for relational programs over all relations and its uniqueness. When dealing with functions the interpreter is modular and obeys the Kahn principle, the authors identify two kinds of anomalies. The first (meagerness anomaly) is caused by the defect of the used processes (computational stations) and holds in fact for arbitrary input-output behaviors. The second (ambiguity anomaly) is rooted in the semantics of relational nets over arbitrary CPO. It is unavoidable in any extension beyond functional behaviors.>