A function on an algebra is congruence preserving if, for any congruence, it maps pairs of congruent elements onto pairs of congruent elements. An algebra is said to be affine complete if every congruence preserving function is a polynomial function. We show that the algebra of (possibly empty) binary trees whose leaves are labeled by letters of an alphabet containing at least one letter, and the free monoid on an alphabet containing at least two letters are affine complete.

Calude, Jain, Khoussainov, Li, and Stephan (2017) proposed a quasi-polynomial-time algorithm solving parity games. After this breakthrough result, a few other quasi-polynomial-time algorithms were introduced; none of them is easy to understand. Moreover, it turns out that in practice they operate very slowly. On the other side there is Zielonka’s recursive algorithm, which is very simple, exponential in the worst case, and the fastest in practice. We combine these two approaches: we propose a small modification of Zielonka’s algorithm, which ensures that the running time is at most quasi-polynomial. In effect, we obtain a simple algorithm that solves parity games in quasi-polynomial time. We also hope that our algorithm, after further optimizations, can lead to an algorithm that shares the good performance of Zielonka’s algorithm on typical inputs, while reducing the worst-case complexity on difficult inputs.

We show that the separation property fails for the classes Σ n of the Rabin-Mostowski index hierarchy of alternating automata on infinite trees. This extends our previous result (obtained with Szczepan Hummel) on the failure of the separation property for the class Σ 2 (i.e., for co-Büchi sets). The non-separation result is also adapted to the analogous classes induced by weak alternating automata.To prove our main result, we first consider the Rabin-Mostowski index hierarchy of deterministic automata on infinite words, for which we give a complete answer (generalizing previous results of Selivanov): the separation property holds for Π n and fails for Σ n -classes. The construction invented for words turns out to be useful for trees via a suitable game.It remains open if the separation property holds for all classes Π n of the index hierarchy for tree automata. To give a positive answer it would be enough to show the reduction property of the dual classes—a method well-known in descriptive set theory. We show that it cannot work here, because the reduction property fails for all classes in the index hierarchy.

We show that the separation property fails for the classes Sigma_n of the Rabin-Mostowski index hierarchy of alternating automata on infinite trees. This extends our previous result (obtained with Szczepan Hummel) on the failure of the separation property for the class Sigma_2 (i.e., for co-Buchi sets). It remains open whether the separation property does hold for the classes Pi_n of the index hierarchy. To prove our result, we first consider the Rabin-Mostowski index hierarchy of deterministic automata on infinite words, for which we give a complete answer (generalizing previous results of Selivanov): the separation property holds for Pi_n and fails for Sigma_n-classes. The construction invented for words turns out to be useful for trees via a suitable game.

Closed monadic /spl Sigma//sub 1/, as proposed in (Ajtai et al., 1998), is the existential monadic second order logic where alternation between existential monadic second order quantifiers and first order quantifiers is allowed. Despite some effort very little is known about the expressive power of this logic on finite structures. We construct a tree automaton which exactly characterizes closed monadic /spl Sigma//sub 1/ on the Rabin tree and give a full analysis of the expressive power of closed monadic /spl Sigma//sub 1/ in this context. In particular we prove that the hierarchy inside closed monadic /spl Sigma//sub 1/, defined by the number of alternations between blocks of first order quantifiers and blocks of existential monadic second order quantifiers collapses, on the infinite tree, to the level 2.

The AltaRica formalism is designed for describing complex systems consisting of a number of interacting components. Its semantics is expressed in terms of transition systems so that a system described in this language can be analysed by any technique or tool applicable to transition systems. The components of a system have two kinds of interactions • event synchronisation, like in the synchronized product of transition systems of Arnold and Nivat, • interface coordination: with each component are associated interfaces whose values depend on the state of the component as well as on the values of interfaces of other components of the system. Another feature of AltaRica is the possibility of defining hierarchical systems: some subsystems can be encapsulated and their mutual interactions as well as their interactions with the rest of the system are supervised by a controller.

Abstract The aim of this paper is to show the use of MEC, an automated tool for analysing transition systems, for discovering deadlocks, livelocks and other properties of a given transition system. The features of MEC are shown with two instructive examples: first, the analysis of an electronic mail system, first analysed by G. Brebner using the concurrency work bench (another automated analysis tool); second, the analysis of a simple call‐processing system originating from Bell‐Northern‐Research.