http://localhost/ojs/regularIssues.phphttp://www.lmcs-online.org/ojs/viewarticle.php?id=301&layout=abstractABSTRACT: In this paper, we consider reachability games over general hybrid systems, and distinguish between two possible observation frameworks for those games: either the precise dynamics of the system is seen by the players (this is the perfect observation framework), or only the starting point and the delays are known by the players (this is the partial observation framework). In the first more classical framework, we show that time-abstract bisimulation is not adequate for solving this problem, although it is sufficient in the case of timed automata . That is why we consider an other equivalence, namely the suffix equivalence based on the encoding of trajectories through words. We show that this suffix equivalence is in general a correct abstraction for games. We apply this result to o-minimal hybrid systems, and get decidability and computability results in this framework. For the second framework which assumes a partial observation of the dynamics of the system, we propose another abstraction, called the superword encoding, which is suitable to solve the games under that assumption. In that framework, we also provide decidability and computability results. http://www.lmcs-online.org/ojs/viewarticle.php?id=531&layout=abstractABSTRACT: Scott's graph model is a lambda-algebra based on the observation thatcontinuous endofunctions on the lattice of sets of natural numbers can berepresented via their graphs. A graph is a relation mapping finite sets ofinput values to output values. We consider a similar model based on relations whose input values are finitesequences rather than sets. This alteration means that we are taking intoaccount the order in which observations are made. This new notion of graphgives rise to a model of affine lambda-calculus that admits an interpretationof imperative constructs including variable assignment, dereferencing andallocation. Extending this untyped model, we construct a category that provides a modelof typed higher-order imperative computation with an affine type system. Anappropriate language of this kind is Reynolds's Syntactic Control ofInterference. Our model turns out to be fully abstract for this language. At aconcrete level, it is the same as Reddy's object spaces model, which was thefirst "state-free" model of a higher-order imperative programming language andan important precursor of games models. The graph model can therefore be seenas a universal domain for Reddy's model.http://www.lmcs-online.org/ojs/viewarticle.php?id=307&layout=abstractABSTRACT: This paper studies colimits of sequences of finite Chu spaces and their ramifications. Besides generic Chu spaces, we consider extensional and biextensional variants. In the corresponding categories we first characterize the monics and then the existence (or the lack thereof) of the desired colimits. In each case, we provide a characterization of the finite objects in terms of monomorphisms/injections. Bifinite Chu spaces are then expressed with respect to the monics of generic Chu spaces, and universal, homogeneous Chu spaces are shown to exist in this category. Unanticipated results driving this development include the fact that while for generic Chu spaces monics consist of an injective first and a surjective second component, in the extensional and biextensional cases the surjectivity requirement can be dropped. Furthermore, the desired colimits are only guaranteed to exist in the extensional case. Finally, not all finite Chu spaces (considered set-theoretically) are finite objects in their categories. This study opens up opportunities for further investigations into recursively defined Chu spaces, as well as constructive models of linear logic.http://www.lmcs-online.org/ojs/viewarticle.php?id=393&layout=abstractABSTRACT: According to a theorem of Courcelle monadic second-order logic and guarded second-order logic (where one can also quantify over sets of edges) have the same expressive power over the class of all countable $k$-sparse hypergraphs. In the first part of the present paper we extend this result to hypergraphs of arbitrary cardinality. In the second part, we present a generalisation dealing with methods to encode sets of vertices by single vertices. http://www.lmcs-online.org/ojs/viewarticle.php?id=481&layout=abstractABSTRACT: Nested words, a model for recursive programs proposed by Alur and Madhusudan,have recently gained much interest. In this paper we introduce quantitativeextensions and study nested word series which assign to nested words elementsof a semiring. We show that regular nested word series coincide with seriesdefinable in weighted logics as introduced by Droste and Gastin. For this weestablish a connection between nested words and the free bisemigroup. Applyingour result, we obtain characterizations of algebraic formal power series interms of weighted logics. This generalizes results of Lautemann, Schwentick andTherien on context-free languages.http://www.lmcs-online.org/ojs/viewarticle.php?id=484&layout=abstractABSTRACT: This article studies the expressive power of finite automata recognizing sets of real numbers encoded in positional notation. We consider Muller automata as well as the restricted class of weak deterministic automata, used as symbolic set representations in actual applications. In previous work, it has been established that the sets of numbers that are recognizable by weak deterministic automata in two bases that do not share the same set of prime factors are exactly those that are definable in the first order additive theory of real and integer numbers. This result extends Cobham's theorem, which characterizes the sets of integer numbers that are recognizable by finite automata in multiple bases. In this article, we first generalize this result to multiplicatively independent bases, which brings it closer to the original statement of Cobham's theorem. Then, we study the sets of reals recognizable by Muller automata in two bases. We show with a counterexample that, in this setting, Cobham's theorem does not generalize to multiplicatively independent bases. Finally, we prove that the sets of reals that are recognizable by Muller automata in two bases that do not share the same set of prime factors are exactly those definable in the first order additive theory of real and integer numbers. These sets are thus also recognizable by weak deterministic automata. This result leads to a precise characterization of the sets of real numbers that are recognizable in multiple bases, and provides a theoretical justification to the use of weak automata as symbolic representations of sets. http://www.lmcs-online.org/ojs/viewarticle.php?id=469&layout=abstractABSTRACT: We study normalising reduction strategies for infinitary Combinatory Reduction Systems (iCRSs). We prove that all fair, outermost-fair, and needed-fair strategies are normalising for orthogonal, fully-extended iCRSs. These facts properly generalise a number of results on normalising strategies in first-order infinitary rewriting and provide the first examples of normalising strategies for infinitary lambda calculus.