Multirelational semantics are well suited to reasoning about programs involving two kinds of non-determinism. This paper lays the categorical foundations for an algebraic calculus of multirelations.

The relative realisability toposes introduced by Awodey, Birkedal and Scott in Awodey et al. (2002) satisfy a universal property involving regular functors to other categories. We use this universal property to define what relative realisability categories are when they are based on categories other than the topos of sets. This paper explains the property and gives a construction for relative realisability categories that works for arbitrary base Heyting categories. The universal property also provides some new geometric morphisms to relative realisability toposes.

In a sequence of papers (Krivine 2001; Krivine 2003; Krivine 2009), J.-L. Krivine introduced his notion of classical realisability for classical second-order logic and Zermelo–Fraenkel set theory. Moreover, in more recent work (Krivine 2008), he has considered forcing constructions on top of it with the ultimate aim of providing a realisability interpretation for the axiom of choice.

The aim of the current paper is to show how Krivine's classical realisability can be understood as an instance of the categorical approach to realisability as started by Martin Hyland in Hyland (1982) and described in detail in van Oosten (2008). Moreover, we will give an intuitive explanation of the iteration of realisability as described in Krivine (2008).

A generalised framework of site graphs is introduced in order to provide the first fully semantic definition of the side-effect-free core of the rule-based language Kappa. This formalisation allows the use of types either to confirm that a rule respects a certain invariant or to guide a restricted refinement process that allows us to constrain its run-time applicability.

We examine a construction due to Fouché in which a Brownian motion is constructed from an algorithmically random infinite binary sequence. We show that although the construction is provably not computable in the sense of computable analysis, a lower bound for the rate of convergence is computable in any upper bound for the compressibilty of the sequence, making the construction layerwise computable.

This paper introduces an endofunctor VT on the category of frames that is parametrised by an endofunctor T on the category Set that satisfies certain constraints. This generalises Johnstone's construction of the Vietoris powerlocale in the sense that his construction is obtained by taking for T the finite covariant power set functor. Our construction of the T-powerlocale VT out of a frame is based on ideas from coalgebraic logic and makes explicit the connection between the Vietoris construction and Moss's coalgebraic cover modality.

We show how to extend certain natural transformations between set functors to natural transformations between T-powerlocale functors. Finally, we prove that the operation VT preserves some properties of frames, such as regularity, zero-dimensionality and the combination of zero-dimensionality and compactness.

The stringent security requirements of organisations like banks or hospitals frequently adopt role-based access control (RBAC) principles to represent and simplify their internal permission management. While representing a fundamental advanced RBAC concept enabling precise restrictions on access rights, authorisation constraints increase the complexity of the resulting security policies so that tool support for convenient creation and adequate validation is required. A particular contribution of our work is a new approach to developing and analysing RBAC policies using a UML-based domain-specific language (DSL), which allows the hiding of the mathematical structures of the underlying authorisation constraints implemented in OCL. The DSL we present is highly configurable and extensible with respect to new concepts and classes of authorisation constraints, and allows the developer to validate RBAC policies in an effective way. The handling of dynamic (that is, time-dependent) constraints, their visual representation through the RBAC DSL and their analysis all form another part of our contribution. The approach is supported by a UML and OCL validation tool.

This paper is concerned with the asymptotic properties of a restricted class of Petri nets equipped with stochastic mass-action semantics. We establish a simple algebraic criterion for the existence of an equilibrium, that is to say, an invariant probability that satisfies the detailed balance condition familiar from the thermodynamics of reaction networks. We also find that when such a probability exists, it can be described by a free energy function that combines an internal energy term and an entropy term. Under strong additional conditions, we show how the entropy term can be deconstructed using the finer-grained individual-token semantics of Petri nets.

String diagrams are a powerful tool for reasoning about physical processes, logic circuits, tensor networks and many other compositional structures. The distinguishing feature of these diagrams is that edges need not be connected to vertices at both ends, and these unconnected ends can be interpreted as the inputs and outputs of a diagram. In this paper, we give a concrete construction for string diagrams using a special kind of typed graph called an open-graph. While the category of open-graphs is not itself adhesive, we introduce the notion of a selective adhesive functor, and show that such a functor embeds the category of open-graphs into the ambient adhesive category of typed graphs. Using this functor, the category of open-graphs inherits ‘enough adhesivity’ from the category of typed graphs to perform double-pushout (DPO) graph rewriting. A salient feature of our theory is that it ensures rewrite systems are ‘type safe’ in the sense that rewriting respects the inputs and outputs. This formalism lets us safely encode the interesting structure of a computational model, such as evaluation dynamics, with succinct, explicit rewrite rules, while the graphical representation absorbs many of the tedious details. Although topological formalisms exist for string diagrams, our construction is discrete and finitary, and enjoys decidable algorithms for composition and rewriting. We also show how open-graphs can be parameterised by graphical signatures, which are similar to the monoidal signatures of Joyal and Street, and define types for vertices in the diagrammatic language and constraints on how they can be connected. Using typed open-graphs, we can construct free symmetric monoidal categories, PROPs and more general monoidal theories. Thus, open-graphs give us a tool for mechanised reasoning in monoidal categories.

Ptolemy‡ is an open-source and extensible modelling and simulation framework. It offers heterogeneous modeling capabilities by allowing different models of computation, both untimed and timed, to be composed hierarchically in an arbitrary fashion. This paper proposes a formal semantics for Ptolemy that is modular in the sense that atomic actors and their compositions are treated in a unified way. In particular, all actors conform to an executable interface that contains four functions: fire (produce outputs given current state and inputs); postfire (update state instantaneously); deadline (how much time the actor is willing to let elapse); and time-update (update the state with the passage of time). Composite actors are obtained using composition operators that in Ptolemy are called directors. Different directors realise different models of computation. In this paper, we formally define the directors for the following models of computation: synchronous- reactive, discrete event, continuous time, process networks and modal models.

The correct and efficient implementation of general real-time applications remains very much an open problem. A key issue is meeting timing constraints whose satisfaction depends on features of the execution platform, in particular its speed. Existing rigorous implementation techniques are applicable to specific classes of systems, for example, with periodic tasks or time-deterministic systems.

We present a general model-based implementation method for real-time systems based on the use of two models:

• • An abstract model representing the behaviour of real-time software as a timed automaton, which describes user-defined platform-independent timing constraints. Its transitions are timeless and correspond to the execution of statements of the real-time software.

• • A physical model representing the behaviour of the real-time software running on a given platform. It is obtained by assigning execution times to the transitions of the abstract model.

We show that, as a rule, physical models are not time-robust, and that time-determinism is a sufficient condition for time-robustness. For a given piece of real-time software and an execution platform corresponding to a time-robust model, we define an execution engine that coordinates the execution of the application software so that it meets its timing constraints. Furthermore, in the case of non-robustness, the execution engine can detect violations of time-safety and stop execution.

We have implemented the execution engine for BIP programs with real-time constraints and validated the implementation method for two case studies. The experimental results for a module of a robotic application show that the CPU utilisation and the size of the model are reduced compared with existing implementations. The experimental results for an adaptive video encoder also show that a lack of time-robustness may seriously degrade the performance for increasing platform execution speed.

We give a complete structural characterisation of the map implemented by the positive branch of a one-way pattern. Our approach is based on the phase map decomposition (de Beaudrap et al. 2006; de Beaudrap et al. 2008) and leads to some preliminary results on the connection between the column structure of a given unitary and the angles of measurements in a pattern that implements it. Our characterisation highlights the role of entanglement in the efficiency of the simulation of a one-way pattern, and it is a step forward towards a full characterisation of those unitaries that have an efficient one-way model implementation.