In this paper we introduce relative formal topology so that we can deal constructively with the closed subsets of a topological space as well as with the open ones. In fact, within standard formal topology, the cover relation allows the definition of the formal opens, which are supposed to act as the formal counterparts of the open subsets, and within balanced formal topology, the binary positivity predicate allows the definition of the formal closed subsets, which are supposed to act as the formal counterparts of the closed subsets. However, these approaches are only fully satisfactory (according to the criterion introduced by the author in Valentini (2005)) if we can provide an adequate formalisation of the cover relation and the positivity predicate. But current formalisations fail in this respect since some intuitionistically valid relations between the open and closed subsets of a concrete topological space cannot be expressed. Our central result is that we can solve this problem through a generalisation of the standard cover relation together with a binary positivity predicate satisfying the positivity axiom.

The analysis of the dynamics of Biological Regulatory Networks (BRNs) requires innovative methods to cope with the state-space explosion. This paper settles an original approach for deciding reachability properties based on Process Hitting, which is a framework suitable for modelling dynamical complex systems. In particular, Process Hitting has been shown to be of interest in providing compact models of the dynamics of BRNs with discrete values. Process Hitting splits a finite number of processes into so-called sorts and describes the way each process is able to act upon (that is, to ‘hit’) another one (or itself) in order to ‘bounce’ it as another process of the same sort with further actions.

By using complementary abstract interpretations of the succession of actions in Process Hitting, we build a very efficient static analysis to over- and under-approximate reachability properties, which avoids the need to build the underlying states graph. The analysis is proved to have a low theoretical complexity, in particular when the number of processes per sorts is limited, while a very large number of sorts can be managed.

This makes such an approach very promising for the scalable analysis of abstract complex systems. We illustrate this through the analysis of a large BRN of 94 components. Our method replies quasi-instantaneously to reachability questions, while standard model-checking techniques regularly fail because of the combinatoric explosion of behaviours.

We introduce a new fragment of linear temporal logic (LTL) called LIO and a new class of Büchi automata (BA) called almost linear Büchi automata (ALBA). We provide effective translations between LIO and ALBA showing that the two formalisms are expressively equivalent. As we expect there to be applications of our results in model checking, we use two standard sources of specification formulae, namely Spec Patterns and BEEM, to study the practical relevance of the LIO fragment, and to compare our translation of LIO to ALBA with two standard translations of LTL to BA using alternating automata. Finally, we demonstrate that the LIO to ALBA translation can be much faster than the standard translation, and the resulting automata can be substantially smaller.

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 .

In this paper we advocate the study of discrete models of social dynamics under adversarial scheduling. The approach we propose forms part of a foundational basis for a generative approach to social science (Epstein 2007). We highlight the feasibility of the adversarial scheduling approach by using it to study the Prisoners's Dilemma Game with Pavlov update, a dynamics that has already been investigated under random update in Kittock (1994), Dyer et al. (2002), Mossel and Roch (2006) and Dyer and Velumailum (2011). The model is specified by letting players at the nodes of an underlying graph G repeatedly play the Prisoner's Dilemma against their neighbours. The players adapt their strategies based on the past behaviour of their opponents by applying the so-called win–stay lose–shift strategy. With random scheduling, starting from any initial configuration, the system reaches the fixed point in which all players cooperate with high probability. On the other hand, under adversarial scheduling the following results hold:

• — A scheduler that can select both game participants can preclude the system from reaching the unique fixed point on most graph topologies.

• — A non-adaptive scheduler that is only allowed to choose one of the participants is no more powerful than a random scheduler. With this restriction, even an adaptive scheduler is not significantly more powerful than the random scheduler, provided it is ‘reasonably fair’.

Using the concept of a generalised priority constraint satisfaction problem, we previously found a way to introduce priority queries into fuzzy relational databases. The results were PFSQL (Priority Fuzzy Structured Query Language) together with a database independent interpreter for it. In an effort to improve the performance of the resolution of PFSQL queries, the aim of the current paper is to formalise PFSQL queries by obtaining their interpretation in an existing fuzzy logic. We have found that the ŁΠ logic provides sufficient elements. The SELECT line of PFSQL queries is semantically a formula of some fuzzy logic, and we show that such formulas can be naturally expressed in a conservative extension of the ŁΠ logic. Furthermore, we prove a theorem that gives the PSPACE containment for the complexity of finding a model for a given ŁΠ logic formula.

Consider the first-order theory of a category.d It has a sort of objects, and a sort of arrows (so we may think of it as a small category). We show that, assuming the principle of unique substitutions, the setoids inside a type theoretic universe provide a model for this first-order theory. We also show that the principle of unique substitutions is not derivable in type theory, but that it is strictly weaker than the principle of unique identity proofs.

We define session types as projections of the behaviour of processes with respect to the operations processes perform on channels. This calls for a parallel composition operator over session types denoting the simultaneous access to a channel by two or more processes. The proposed approach allows us to define a semantically grounded theory of session types that does not require the linear usage of channels. However, type preservation and progress can only be guaranteed for processes that never receive channels they already own. A number of examples show that the resulting framework validates existing session-type theories and unifies them to some extent.

In this paper we propose various extensions to the relational model to support similarity-based querying. We build upon the -relation model, where tuples are assigned values from an arbitrary semiring , and its associated positive relational algebra . We consider a recently proposed extension to using a monus operation on the semiring to support negative queries, and show how, surprisingly, it fails for important ‘fuzzy’ semirings. Instead, we suggest using a negation operator. We also consider the identities satisfied by the relational algebra . We show that moving from a semiring to a particular form of lattice (a De Morgan frame) yields a relational algebra that satisfies all the classical (positive) relational algebra identities. We claim that to support real-world similarity queries realistically, one must move from tuple-level annotations to attribute-level annotations. We show in detail how our De Morgan frame-based model can be extended to support attribute-level annotations and give worked examples of similarity queries in this setting.

In this paper we address the extension problem for quantal measures of path-integral type, concentrating on two cases: sequential growth of causal sets and a particle moving on the finite lattice ℤn. In both cases, the dynamics can be coded into a vector-valued measure μ on Ω, the space of all histories. Initially, μ is just defined on special subsets of Ω called cylinder events, and we would like to extend it to a larger family of subsets (events) in analogy to the way this is done in the classical theory of stochastic processes. Since quantally μ is generally not of bounded variation, a new method is required. We propose a method that defines the measure of an event by means of a sequence of simpler events that in a suitable sense converges to the event whose measure we are seeking to define. To this end, we introduce canonical sequences approximating certain events, and we propose a measure-based criterion for the convergence of such sequences. Applying the method, we encounter a simple event whose measure is zero classically but non-zero quantally.

In this short note we study the semantics of two basic computational effects, exceptions and states, from a new point of view. In the handling of exceptions we dissociate the control from the elementary operation that recovers from the exception. In this way it becomes apparent that there is a duality, in the categorical sense, between exceptions and states.

This paper presents a bisimulation-based method for establishing the soundness of equations between terms constructed using operations whose semantics are specified by rules in the GSOS format of Bloom, Istrail and Meyer. The method is inspired by de Simone's FH-bisimilarity and uses transition rules as schematic transitions in a bisimulation-like relation between open terms. The soundness of the method is proved and examples showing its applicability are provided. The proposed bisimulation-based proof method is incomplete, but we do offer some completeness results for restricted classes of GSOS specifications. An extension of the proof method to the setting of GSOS languages with predicates is also offered.

Van Glabbeek and Goltz (and later Fecher) have investigated the relationships between various equivalences on stable configuration structures, including interleaving bisimulation (IB), step bisimulation (SB), pomset bisimulation and hereditary history-preserving (H-H) bisimulation. Since H-H bisimulation may be characterised by the use of reverse as well as forward transitions, it is of interest to investigate these and other forms of bisimulations where both forward and reverse transitions are allowed. Bednarczyk asked whether SB with reverse steps is as strong as H-H bisimulation. We answer this question negatively. We give various characterisations of SB with reverse steps, showing that forward steps do not add power. We strengthen Bednarczyk's result that, in the absence of auto-concurrency, reverse IB is as strong as H-H bisimulation, by showing that we need only exclude auto-concurrent events at the same depth in the configuration.

We consider several other forms of observations of reversible behaviour and define a wide range of bisimulations by mixing the forward and reverse observations. We investigate the power of these bisimulations and represent the relationships between them as a hierarchy with IB at the bottom and H-H at the top.