We consider computation with real numbers that arise through a process of physical measurement. We have developed a theory in which physical experiments that measure quantities can be used as oracles to algorithms and we have begun to classify the computational power of various forms of experiment using non-uniform complexity classes. Earlier, in Beggs et al. (2014 Reviews of Symbolic Logic7(4) 618–646), we observed that measurement can be viewed as a process of comparing a rational number z – a test quantity – with a real number y – an unknown quantity; each oracle call performs such a comparison. Experiments can then be classified into three categories, that correspond with being able to return test results $$\begin{eqnarray*} z < y\text{ or }z > y\text{ or }\textit{timeout},\\ z < y\text{ or }\textit{timeout},\\ z \neq y\text{ or }\textit{timeout}. \end{eqnarray*} $$ These categories are called two-sided, threshold and vanishing experiments, respectively. The iterative process of comparing generates a real number y. The computational power of two-sided and threshold experiments were analysed in several papers, including Beggs et al. (2008 Proceedings of the Royal Society, Series A (Mathematical, Physical and Engineering Sciences)464 (2098) 2777–2801), Beggs et al. (2009 Proceedings of the Royal Society, Series A (Mathematical, Physical and Engineering Sciences)465 (2105) 1453–1465), Beggs et al. (2013a Unconventional Computation and Natural Computation (UCNC 2013), Springer-Verlag 6–18), Beggs et al. (2010b Mathematical Structures in Computer Science20 (06) 1019–1050) and Beggs et al. (2014 Reviews of Symbolic Logic, 7 (4):618-646). In this paper, we attack the subtle problem of measuring physical quantities that vanish in some experimental conditions (e.g., Brewster's angle in optics). We analyse in detail a simple generic vanishing experiment for measuring mass and develop general techniques based on parallel experiments, statistical analysis and timing notions that enable us to prove lower and upper bounds for its computational power in different variants. We end with a comparison of various results for all three forms of experiments and a suitable postulate for computation involving analogue inputs that breaks the Church–Turing barrier.

What can algorithms compute with the help of information provided by an oracle that is a physical system? We have developed a theory that combines Turing machines with experiments that perform physical measurements in which queries are governed by subtle timing protocols and provide the equipment with numerical data with (i) infinite precision, (ii) finite but unbounded precision or (iii) finite but fixed precision. Here, we consider the measurement of physical quantities that are thresholds, whose values are obtained by a sequence of approximate measurements that converge either from above or from below. The thresholds may be authentic physical properties or artefacts of the methods and equipment that performs the measurement. Using a canonical example of a threshold oracle, the broken beam balance for measuring mass, we develop methods to cope with thresholds and classify the computational power in polynomial time of this physical oracle using non-uniform complexity classes. Surprisingly, new complexity classes arise illuminating the influence of the operation of the equipment. All classes break the Turing Barrier.

In this article, we show that once we assume that there is some uniformity in Nature, empirical laws and theories involving the concepts of Physics can be learned by the scientists. We develop a mathematical framework to explain learnability of empirical relations. Then we classify the degree of learnability according to the degree of predictability by means of timescales. We also use the same mathematical framework to make formal the claim that learnability evolves according not only with the number of observations done, but also with the precision of measurements.

Using physical experiments as oracles for algorithms, we can characterise the computational power of classes of physical systems. Here we show that two different physical models of the apparatus for a single experiment can have different computational power. The experiment is thescatter machine experiment(SME), which was first presented in Beggs and Tucker (2007b). Our first physical model contained a wedge with a sharp vertex that made the experiment non-deterministic with constant runtime. We showed that Turing machines with polynomial time and an oracle based on a sharp wedge computed the non-uniform complexity classP/poly. Here we reconsider the experiment with a refined physical model where the sharp vertex of the wedge is replaced byanysuitable smooth curve with vertex at the same point. These smooth models of the experimental apparatus are deterministic. We show thatno matter what shape is chosen for the apparatus: (i) the time of detection of the scattered particles increases at least exponentially with the size of the query; and (ii) Turing machines with polynomial time and an oracle based on a smooth wedge compute the non-uniform complexity classP/log* ⫋P/poly. We discuss evidence that many experiments that measure quantities have exponential runtimes and a computational power ofP/log*.

We pose the following question: If a physical experiment were to be completely controlled by an algorithm, what effect would the algorithm have on the physical measurements made possible by the experiment? In a programme to study the nature of computation possible by physical systems, and by algorithms coupled with physical systems, we have begun to analyse: (i) the algorithmic nature of experimental procedures; and (ii) the idea of using a physical experiment as an oracle to Turing Machines. To answer the question, we will extend our theory of experimental oracles so that we can use Turing machines to model the experimental procedures that govern the conduct of physical experiments. First, we specify an experiment that measures mass via collisions in Newtonian dynamics and examine its properties in preparation for its use as an oracle. We begin the classification of the computational power of polynomial time Turing machines with this experimental oracle using non-uniform complexity classes. Second, we show that modelling an experimenter and experimental procedure algorithmically imposes a limit on what can be measured using equipment. Indeed, the theorems suggest a new form of uncertainty principle for our knowledge of physical quantities measured in simple physical experiments. We argue that the results established here are representative of a huge class of experiments.

In “Petti nets are Monoids” by Meseguer and Montanari, categories for Petri nets with and without markings are introduced, where the categorical product and coproduct express the joint behavior of nets. However, this framework lacks structure in the sense that there is no categorical technique to define a composition of nets satisfying some given synchronization specification. In this paper, a synchronization operation is proposed which is a functor induced by some given synchronization prescription at the transition level. Moreover, since this operation is also able to represent the asynchronous composition, the fact that some categories of Petri nets lack coproducts (asynchronous composition) is not anymore a restriction for interaction semantics.

Summary Since Pnueli’s seminal paper in 1977, Temporal Logic has been used as a formalism for specifying and verifying the correctness of reactive systems. In this paper, we show that, besides its expressive power, Temporal Logic enjoys a very strong structural property: it is categorical on processes. That is, we show how temporal specifications (as theories) can be embedded in categories of process behaviour, and out of this adjunction we build an institution that is categorical in the sense of Meseguer. This characterisation means that temporal logic is, in a sense, ‘sound and complete’ with respect to process specification and interconnection techniques.

Abstract A denotational semantics and a sound and complete inequational proof systems for processes with varying degrees of liveness is presented. New insights on quiescence are given concerning the Jonsson characterisation of input/output system. A theory of transational behaviour of the type carry out until the end is developed as an application of this concept of process with liveness requirements. The proposed model fully reflects the parallel composition of transactional requirements , giving the expected composite requirements.

A logic for specifying and reasoning about object classes and their instances (aspects) is presented and illustrated. This logic is an extension of a rather standard linear temporal, many-sorted, first-order predicate logic with equality. The extensions were designed to be as simple as possible while supporting the envisaged locality of arguments, object specialization and object aggregation. Objects are specified through their aspects. Each aspect establishes a local vocabulary (signature). The logic works at two levels: first, we can specify and prove assertions about a given object aspect in isolation (local reasoning), e.g. persons, patients or cars; second, we can specify interaction constraints and make inferences between aspects within the same community of objects (global reasoning), e.g. carry the theorems of persons onto patients (specialization inheritance) or carry the theorems of persons onto the aggregations of persons and cars (incorporation inheritance). Some reflection mechanisms are also shown to be sound: for instance what becomes true of persons because of the interactions between persons and cars. The proposed logic is given in an axiomatic style.