This paper introduces a temporal logic for coalgebras. Nexttime and lasttime operators are defined for a coalgebra, acting on predicates on the state space. They give rise to what is called a Galois algebra. Galois algebras form models of temporal logics like Linear Temporal Logic (LTL) and Computation Tree Logic (CTL). The mapping from coalgebras to Galois algebras turns out to be functorial, yielding indexed categorical structures. This construction gives many examples, for coalgebras of polynomial functors on sets. More generally, it will be shown how ‘fuzzy’ predicates on metric spaces, and predicates on presheaves, yield indexed Galois algebras, in basically the same coalgebraic manner.

The spatial search problem consists of minimising the number of steps required to find a given site in a network, with the restriction that only an oracle query or a translation to a neighbouring site is allowed at each step. We propose a quantum algorithm for the spatial search problem on a triangular lattice with N sites and torus-like boundary conditions. The proposed algorithm is a special case of the general framework for abstract search proposed by Ambainis, Kempe and Rivosh (AKR) in Ambainis et al. (2005) and Tulsi in Tulsi (2008) applied to a triangular network. The AKR–Tulsi formalism was employed to show that the time complexity of the quantum search on the triangular lattice is .

We show how the principal typing property of the rank 2 intersection type system enables the specification of a modular and polyvariant control-flow analysis.

Delta modelling is an approach to facilitate the automated product derivation for software product lines. It is based on a set of deltas specifying modifications that are incrementally applied to a core product. The applicability of deltas depends on application conditions over features. This paper presents abstract delta modelling, which explores delta modelling from an abstract, algebraic perspective. Compared to the previous work, we take a more flexible approach to conflicts between modifications by introducing the notion of conflict-resolving deltas. Furthermore, we extend our approach to allow the nesting of delta models for increased modularity. We also present conditions on the structure of deltas to ensure unambiguous product generation.

The order-enriched category of monotonic predicate transformers over posets is a model of the refinement calculus of higher order imperative programs and pre-post specifications. This category is shown to be equivalent to the category of spans over ideal relations, and ideal relations are shown to be spans over monotonic functions between posets. To do this we use a skew span construction because the standard categorical span constructions are inapplicable. Axioms are given for products and coproducts of underlying posets as well as the homset as a coexponent, using inequations (for various kinds of lax adjunctions) and conditional equations (for adjunctions in subcategories) that are shown to uniquely determine the structures. The model is described in elementary terms using power allegories, an axiomatic calculus of relations, which makes the proofs accessible to non-specialists and shows that the results generalize to other base categories.

Non-commutative logic, which is a unification of commutative linear logic and cyclic linear logic, is extended to all linear connectives: additives, exponentials and constants. We give two equivalent versions of the sequent calculus (directly with the structure of order varieties, and with their presentations as partial orders), phase semantics and a cut-elimination theorem. This involves, in particular, the study of the entropy relation between partial orders, and the introduction of a special class of order varieties: the series–parallel order varieties.

We present a result of C.C. Squier relating two topics:

— the canonical rewriting systems, which have been widely studied by computer scientists as a tool for solving word problems,

— the homology of groups (more generally of monoids), which belongs to the core of pure mathematics, on the borders of algebra and topology.

We present an algorithm for deciding polarised higher-order subtyping without bounded quantification. Constructors are identified not only modulo β, but also η. We give a direct proof of completeness, without constructing a model or establishing a strong normalisation theorem. Inductive and coinductive types are enriched with a notion of size and the subtyping calculus is extended to account for the inclusions arising between the sized types.

This special issue of Mathematical Structures in Computer Science contains several contributions related to the modern field of Quantum Information and Quantum Computing.

The first two papers deal with entanglement. The paper by R. Mosseri and P. Ribeiro presents a detailed description of the two- and three-qubit geometry in Hilbert space, dealing with the geometry of fibrations and discrete geometry. The paper by J.-G.Luque et al. is more algebraic and considers invariants of pure k-qubit states and their application to entanglement measurement.

We study autostability spectra relative to strong constructivizations (SC-autostability spectra). For a decidable structure $\mathcal{S}$, the SC-autostability spectrum of $\mathcal{S}$ is the set of all Turing degrees capable of computing isomorphisms among arbitrary decidable copies of $\mathcal{S}$. The degree of SC-autostability for $\mathcal{S}$ is the least degree in the spectrum (if such a degree exists).

We prove that for a computable successor ordinal α, every Turing degree c.e. in and above 0(α) is the degree of SC-autostability for some decidable structure. We show that for an infinite computable ordinal β, every Turing degree c.e. in and above 0(2β+1) is the degree of SC-autostability for some discrete linear order. We prove that the set of all PA-degrees is an SC-autostability spectrum. We also obtain similar results for autostability spectra relative to n-constructivizations.

We provide a consistent way of looking at a range of finite state machines and their algebraic models. Our claim is that the natural representation of transitions of finite state machines is in terms of monoid homomorphisms, and distinct generalisation processes that can be applied to finite state machines correspond to distinct categorical generalisation processes at the level of the algebraic models.

The generalisations we consider are those from deterministic to non-deterministic machines, from one-way to two-way machines, and from read-only machines to read/write machines. Hence the finite state machines we consider, and provide algebraic models for, are (deterministic and non-deterministic) finite state automata, two-way automata, Mealy machines, and bounded Turing machines.

The categorical constructions corresponding to these generalisation processes are, respectively: altering the base category from functions to relations, applying the Geometry of Interaction, or Int construction, and a categorical process, which we refer to as the Comp construction, that uses the tensor on monoidal categories to construct graded categories.

In the first part of this paper (Duval and Reynaud 1994), we defined a categorical framework, based on the notion of sketch, for specification and evaluation in the senses of algebraic specifications and algebraic programming. Static evaluation in quasi-projective sketches was defined in Part I; in this paper, dynamic evaluation is introduced. It deals with more general structures, which may have no initial model. Until now, this process has not been used in algebraic specification systems, but computer algebra systems are beginning to use it as a basic tool. Finally, we give some applications of dynamic evaluation to computation in field extensions.

We give an algorithm allowing the construction of bases of local unitary invariants of pure k-qubit states from a knowledge of the polynomial covariants of the group of invertible local filtering operations. The simplest invariants obtained in this way are made explicit and compared with various known entanglement measures. Complete sets of generators are obtained for up to four qubits, and the structure of the invariant algebras is discussed in detail.

We consider a calculus for multiparty sessions enriched with security levels for messages. We propose a monitored semantics for this calculus, which blocks the execution of processes as soon as they attempt to leak information. We illustrate the use of this semantics with various examples, and show that the induced safety property is compositional and that it is strictly included between a typability property and a security property proposed for an extended calculus in previous work.

The strict globular ω-categories formalize the execution paths of a parallel automaton and the homotopies between them. One associates to such (and any) ω-category [Cscr ] three homology theories. The first one is called the globular homology. It contains the oriented loops of [Cscr ]. The two other ones are called the negative (respectively, positive) corner homology. They contain in a certain manner the branching areas of execution paths or negative corners (respectively, the merging areas of execution paths or positive corners) of [Cscr ]. Two natural linear maps called the negative (respectively, the positive) Hurewicz morphism from the globular homology to the negative (respectively, positive) corner homology are constructed. We explain the reason why these constructions allow the reinterpretation of some geometric problems coming from computer science.

The effective use of model-based formal methods in the development of complex embedded systems requires the integration of discrete-event models of controllers with continuous-time models of their environments. This paper proposes a new approach to the development of such combined models (co-models), in which an initial discrete-event model may include approximations of continuous-time behaviour that can subsequently be replaced by couplings to continuous-time models. An operational semantics of co-simulation allows the discrete and continuous models to run on their respective simulators and managed by a coordinating co-simulation engine. This permits the exploration of the composite co-model's behaviour in a range of operational scenarios. The approach has been realised using the Vienna Development Method (VDM) as the discrete-event formalism, and 20-sim as the continuous-time framework, and has been applied successfully to a case study based on the distributed controller for a personal transporter device.

We show that real-number computations in the interval-domain environment are ‘inherently parallel’ in a precise mathematical sense. We do this by reducing computations of the weak parallel-or operation on the Sierpinski domain to computations of the addition operation on the interval domain.

In this paper we consider general probabilistic theories pertaining to circuits that satisfy two very natural assumptions. We provide a formalism that is local in the following very specific sense: calculations pertaining to any region of space–time employ only mathematical objects associated with that region. We call this formalism locality. It incorporates the idea that space and time should be treated on an equal footing. Formulations that use a foliation of space--time to evolve a state do not have this property, nor do histories-based approaches. An operation has inputs and outputs (through which systems travel), for example,

We introduce convex–concave duality for various models of non-deterministic choice, probabilistic choice and the two of them combined. This complements the well-known duality of stably compact spaces in a pleasing way: convex–concave duality swaps angelic and demonic choice, and leaves probabilistic choice invariant.

We use some results of Trnková to show first that subcoalgebras are always closed under finite intersections. Assuming that the type functor F is bounded, we obtain a concrete representation of the terminal F-coalgebra. We also provide several equivalent characterizations of boundedness.