Catálogo de publicaciones - libros

We present a general framework for logics of transition systems based on Stone duality. Transition systems are modelled as coalgebras for a functor T on a category χ . The propositional logic used to reason about state spaces from χ is modelled by the Stone dual ${\mathcal A}$ of χ (e.g. if χ is Stone spaces then ${\mathcal A}$ is Boolean algebras and the propositional logic is the classical one). In order to obtain a modal logic for transition systems (i.e. for T -coalgebras) we consider the functor L on ${\mathcal A}$ that is dual to T . An adequate modal logic for T -coalgebras is then obtained from the category of L -algebras which is, by construction, dual to the category of T -coalgebras. The logical meaning of the duality is that the logic is sound and complete and expressive (or fully abstract) in the sense that non-bisimilar states are distinguished by some formula. We apply the framework to Vietoris coalgebras on topological spaces, using the duality between spaces and observation frames, to obtain adequate logics for transition systems on posets, sets, spectral spaces and Stone spaces.

Term rewriting systems provide a versatile model of computation. An important property which allows to abstract from potential nondeterminism of parallel execution of the modelled program is confluence. In this paper we prove that confluence of a fairly large class of systems, namely right ground term rewriting systems, is decidable. We introduce a labelling of variables with colours and constrain substitutions according to these colours. We show how right ground rewriting systems can be reduced to simple systems with coloured variables. Such systems can be analysed using reduction-automata techniques which leads to an interesting decision procedure for confluence.

Recent work by Knapik, Niwiński and Urzyczyn (in FOSSACS 2002) has revived interest in the connexions between higher-order grammars and higher-order pushdown automata. Both devices can be viewed as definitions for term trees as well as string languages. In the latter setting we recall the extensive study by Damm (1982), and Damm and Goerdt (1986). There it was shown that a language is accepted by a level- n pushdown automaton if and only if the language is generated by a safe level- n grammar. We show that at level 2 the safety assumption may be removed. It follows that there are no inherently unsafe string languages at level 2.

We introduce a domain-theoretic computational model for multi-variable differential calculus, which for the first time gives rise to data types for differentiable functions. The model, a continuous Scott domain for differentiable functions of n variables, is built as a sub-domain of the product of n + 1 copies of the function space on the domain of intervals by tupling together consistent information about locally Lipschitz (piecewise differentiable) functions and their differential properties (partial derivatives). The main result of the paper is to show, in two stages, that consistency is decidable on basis elements, which implies that the domain can be given an effective structure. First, a domain-theoretic notion of line integral is used to extend Green’s theorem to interval-valued vector fields and show that integrability of the derivative information is decidable. Then, we use techniques from the theory of minimal surfaces to construct the least and the greatest piecewise linear functions that can be obtained from a tuple of n + 1 rational step functions, assuming the integrability of the n -tuple of the derivative part. This provides an algorithm to check consistency on the rational basis elements of the domain, giving an effective framework for multi-variable differential calculus.