-
On human-centred security: A new systems model based on modes and mode transitions
Authors:
Edwin J Beggs,
John V Tucker,
Victoria Wang
Abstract:
We propose an abstract conceptual framework for analysing complex security systems using a new notion of modes and mode transitions. A mode is an independent component of a system with its own objectives, monitoring data, algorithms, and scope and limits. The behaviour of a mode, including its transitions to other modes, is determined by interpretations of the mode's monitoring data in the light o…
▽ More
We propose an abstract conceptual framework for analysing complex security systems using a new notion of modes and mode transitions. A mode is an independent component of a system with its own objectives, monitoring data, algorithms, and scope and limits. The behaviour of a mode, including its transitions to other modes, is determined by interpretations of the mode's monitoring data in the light of its objectives and capabilities -- these interpretations we call beliefs. We formalise the conceptual framework mathematically and, by quantifying and visualising beliefs in higher-dimensional geometric spaces, we argue our models may help both design, analyse and explain systems. The mathematical models are based on simplicial complexes.
△ Less
Submitted 3 May, 2024;
originally announced May 2024.
-
Rings with common division, common meadows and their conditional equational theories
Authors:
Jan A Bergstra,
John V Tucker
Abstract:
We examine the consequences of having a total division operation $\frac{x}{y}$ on commutative rings. We consider two forms of binary division, one derived from a unary inverse, the other defined directly as a general operation; each are made total by setting $1/0$ equal to an error value $\bot$, which is added to the ring. Such totalised divisions we call common divisions. In a field the two forms…
▽ More
We examine the consequences of having a total division operation $\frac{x}{y}$ on commutative rings. We consider two forms of binary division, one derived from a unary inverse, the other defined directly as a general operation; each are made total by setting $1/0$ equal to an error value $\bot$, which is added to the ring. Such totalised divisions we call common divisions. In a field the two forms are equivalent and we have a finite equational axiomatisation $E$ that is complete for the equational theory of fields equipped with common division, called common meadows. These equational axioms $E$ turn out to be true of commutative rings with common division but only when defined via inverses. We explore these axioms $E$ and their role in seeking a completeness theorem for the conditional equational theory of common meadows. We prove they are complete for the conditional equational theory of commutative rings with inverse based common division. By adding a new proof rule, we can prove a completeness theorem for the conditional equational theory of common meadows. Although, the equational axioms $E$ fail with common division defined directly, we observe that the direct division does satisfies the equations in $E$ under a new congruence for partial terms called eager equality.
△ Less
Submitted 26 May, 2024; v1 submitted 2 May, 2024;
originally announced May 2024.
-
A Complete Finite Axiomatisation of the Equational Theory of Common Meadows
Authors:
Jan A Bergstra,
John V Tucker
Abstract:
We analyse abstract data types that model numerical structures with a concept of error. Specifically, we focus on arithmetic data types that contain an error value $\bot$ whose main purpose is to always return a value for division. To rings and fields, we add a division operator $x/y$ and study a class of algebras called common meadows wherein $x/0 = \bot$. The set of equations true in all common…
▽ More
We analyse abstract data types that model numerical structures with a concept of error. Specifically, we focus on arithmetic data types that contain an error value $\bot$ whose main purpose is to always return a value for division. To rings and fields, we add a division operator $x/y$ and study a class of algebras called common meadows wherein $x/0 = \bot$. The set of equations true in all common meadows is named the equational theory of common meadows. We give a finite equational axiomatisation of the equational theory of common meadows and prove that it is complete and that the equational theory is decidable.
△ Less
Submitted 26 May, 2024; v1 submitted 9 July, 2023;
originally announced July 2023.
-
The dynamics of belief: continuously monitoring and visualising complex systems
Authors:
Edwin J. Beggs,
John V. Tucker
Abstract:
The rise of AI in human contexts places new demands on automated systems to be transparent and explainable. We examine some anthropomorphic ideas and principles relevant to such accountablity in order to develop a theoretical framework for thinking about digital systems in complex human contexts and the problem of explaining their behaviour. Structurally, systems are made of modular and hierachica…
▽ More
The rise of AI in human contexts places new demands on automated systems to be transparent and explainable. We examine some anthropomorphic ideas and principles relevant to such accountablity in order to develop a theoretical framework for thinking about digital systems in complex human contexts and the problem of explaining their behaviour. Structurally, systems are made of modular and hierachical components, which we abstract in a new system model using notions of modes and mode transitions. A mode is an independent component of the system with its own objectives, monitoring data, and algorithms. The behaviour of a mode, including its transitions to other modes, is determined by functions that interpret each mode's monitoring data in the light of its objectives and algorithms. We show how these belief functions can help explain system behaviour by visualising their evaluation as trajectories in higher-dimensional geometric spaces. These ideas are formalised mathematically by abstract and concrete simplicial complexes. We offer three techniques: a framework for design heuristics, a general system theory based on modes, and a geometric visualisation, and apply them in three types of human-centred systems.
△ Less
Submitted 17 January, 2024; v1 submitted 11 August, 2022;
originally announced August 2022.
-
A model of systems with modes and mode transitions
Authors:
Edwin Beggs,
John V. Tucker
Abstract:
We propose a method of classifying the operation of a system into finitely many modes. Each mode has its own objectives for the system's behaviour and its own mathematical models and algorithms designed to accomplish its objectives. A central problem is deciding when to transition from one mode to some other mode, a decision that may be contested and involve partial or inconsistent information or…
▽ More
We propose a method of classifying the operation of a system into finitely many modes. Each mode has its own objectives for the system's behaviour and its own mathematical models and algorithms designed to accomplish its objectives. A central problem is deciding when to transition from one mode to some other mode, a decision that may be contested and involve partial or inconsistent information or evidence. We model formally the concept of modes for a system and derive a family of data types for analysing mode transitions. The data types are simplicial complexes, both abstract and realised in euclidean space $\mathbb{R}^{n}$. In the data type, a mode is represented by a simplex. Each state of a system can be evaluated relative to different modes by map** it into one or more simplices. This calibration measures the extent to which distinct modes are appropriate for the state and can decide on a transition. We explain this methodology based on modes, introduce the mathematical ideas about simplicial objects we need and use them to build a theoretical framework for modes and mode transitions. To illustrate the general model in some detail, we work though a case study of an autonomous racing car.
△ Less
Submitted 13 July, 2021;
originally announced July 2021.
-
An algebraic theory for data linkage
Authors:
Liang-Ting Chen,
Markus Roggenbach,
John V. Tucker
Abstract:
There are countless sources of data available to governments, companies, and citizens, which can be combined for good or evil. We analyse the concepts of combining data from common sources and linking data from different sources. We model the data and its information content to be found in a single source by a partial ordered monoid, and the transfer of information between sources by different typ…
▽ More
There are countless sources of data available to governments, companies, and citizens, which can be combined for good or evil. We analyse the concepts of combining data from common sources and linking data from different sources. We model the data and its information content to be found in a single source by a partial ordered monoid, and the transfer of information between sources by different types of morphisms. To capture the linkage between a family of sources, we use a form of Grothendieck construction to create a partial ordered monoid that brings together the global data of the family in a single structure. We apply our approach to database theory and axiomatic structures in approximate reasoning. Thus, partial ordered monoids provide a foundation for the algebraic study for information gathering in its most primitive form.
△ Less
Submitted 12 October, 2018;
originally announced October 2018.
-
Analogue-digital systems and the modular decomposition of physical behaviour
Authors:
E. J. Beggs,
J. V. Tucker
Abstract:
We take a fresh look at analogue-digital systems focussing on their physical behaviour. We model a general analogue-digital system as a physical process controlled by an algorithm by viewing the physical process as physical oracle to the algorithm, generalising the notion of Turing. We develop a theoretical framework for the specification and analysis of such systems that combines five semantical…
▽ More
We take a fresh look at analogue-digital systems focussing on their physical behaviour. We model a general analogue-digital system as a physical process controlled by an algorithm by viewing the physical process as physical oracle to the algorithm, generalising the notion of Turing. We develop a theoretical framework for the specification and analysis of such systems that combines five semantical notions: actual physical behaviour, measured behaviour, predicted behaviour, computed behaviour and exceptional behaviour. Next, we consider the more general and applicable situation of complex processes that exhibit several distinct modes of physical behaviour. Thus, for their design, a set of mathematical models may be needed, each model having its own domain of application and representing a particular mode of behaviour or operation of physical reality with its own physical oracle. The models may be of disparate kinds and, furthermore, not all physical modes may even have a reliable model. We address the questions: How do we specify algorithms and software that monitor or govern a complex physical situation with many physical modes? How do we specify a portfolio of modes, and the computational problem of transitioning from using one mode to another mode as physical behaviour changes? We propose a general definition of an analogue-digital system with modes, and show how any diverse set of modes, with or without models, can be bound together, and how the transitions between modes can be determined, by constructing a data type and mode selection functions. We illustrate the ideas of physical modes and our theory by reflecting on simple examples, including driverless racing cars.
△ Less
Submitted 16 April, 2018;
originally announced April 2018.
-
Monitoring and Intervention: Concepts and Formal Models
Authors:
Kenneth Johnson,
John V. Tucker,
Victoria Wang
Abstract:
Our machines, products, utilities, and environments have long been monitored by embedded software systems. Our professional, commercial, social and personal lives are also subject to monitoring as they are mediated by software systems. Data on nearly everything now exists, waiting to be collected and analysed for all sorts of reasons. Given the rising tide of data we pose the questions: What is mo…
▽ More
Our machines, products, utilities, and environments have long been monitored by embedded software systems. Our professional, commercial, social and personal lives are also subject to monitoring as they are mediated by software systems. Data on nearly everything now exists, waiting to be collected and analysed for all sorts of reasons. Given the rising tide of data we pose the questions: What is monitoring? Do diverse and disparate monitoring systems have anything in common? We attempt answer these questions by proposing an abstract conceptual framework for studying monitoring. We argue that it captures a structure common to many different monitoring practices, and that from it detailed formal models can be derived, customised to applications. The framework formalises the idea that monitoring is a process that observes the behaviour of people and objects in a context. The entities and their behaviours are represented by abstract data types and the observable attributes by logics. Since monitoring usually has a specific purpose, we extend the framework with protocols for detecting attributes or events that require interventions and, possibly, a change in behaviour. Our theory is illustrated by a case study from criminal justice, that of electronic tagging.
△ Less
Submitted 25 January, 2017;
originally announced January 2017.
-
Analogue-digital systems with modes of physical behaviour
Authors:
Edwin Beggs,
John V. Tucker
Abstract:
Complex environments, processes and systems may exhibit several distinct modes of physical behaviour or operation. Thus, for example, in their design, a set of mathematical models may be needed, each model having its own domain of application and representing a particular mode of behaviour or operation of physical reality. The models may be of disparate kinds { discrete or continuous in data, time…
▽ More
Complex environments, processes and systems may exhibit several distinct modes of physical behaviour or operation. Thus, for example, in their design, a set of mathematical models may be needed, each model having its own domain of application and representing a particular mode of behaviour or operation of physical reality. The models may be of disparate kinds { discrete or continuous in data, time and space. Furthermore, some physical modes may not have a reliable model. Physical measurements determine modes of operation. We explore the question: What is a mode of behaviour? How do we specify algorithms and software that monitor or govern a complex physical situation with many modes? How do we specify a portfolio of modes, and the computational problem of transitioning from using one mode to another mode as physical modes change? We propose a general definition of an analogue-digital system with modes. We show how any diverse set of modes { with or without models { can be bound together, and how the transitions between modes can be determined, by constructing a topological data type based upon a simplicial complex. We illustrate the ideas of physical modes and our theory by reflecting on simple examples, including driverless racing cars.
△ Less
Submitted 26 October, 2016; v1 submitted 8 December, 2014;
originally announced December 2014.
-
Formalising Surveillance and Identity
Authors:
Victoria Wang,
John V. Tucker
Abstract:
Surveillance is a social phenomenon that is general and commonplace, employed by governments, companies and communities. Its ubiquity is due to technologies for gathering and processing data; its strong and obvious effects raise difficult social questions. We give a general definition of surveillance that captures the notion in diverse situations and we illustrate it with some disparate examples.A…
▽ More
Surveillance is a social phenomenon that is general and commonplace, employed by governments, companies and communities. Its ubiquity is due to technologies for gathering and processing data; its strong and obvious effects raise difficult social questions. We give a general definition of surveillance that captures the notion in diverse situations and we illustrate it with some disparate examples.A most important, if neglected,component idea is that of the identity of the people or objects observed. We propose a general definition of identifiers as data designed to specify the identity of an entity in some context or for some purpose. We examine the ways identifiers depend upon other identifiers and show the provenance of identifiers requires reductions between identifiers and a special idea of personal identifier. The theory is formalised mathematically. Finally, we reflect on the role of formal methods to give insights in sociological contexts.
△ Less
Submitted 14 August, 2014;
originally announced August 2014.
-
On the Role of Identity in Surveillance
Authors:
Victoria Wang,
John V. Tucker
Abstract:
Surveillance is a process that observes behaviour, recognises properties and identifies individuals. It has become a commonplace phenomenon in our everyday life. Many surveillance practices depend on the use of advanced technologies to collect, store and process data. We propose (i) an abstract definition of surveillance; and (ii) an abstract definition of identity, designed to capture the common…
▽ More
Surveillance is a process that observes behaviour, recognises properties and identifies individuals. It has become a commonplace phenomenon in our everyday life. Many surveillance practices depend on the use of advanced technologies to collect, store and process data. We propose (i) an abstract definition of surveillance; and (ii) an abstract definition of identity, designed to capture the common structure of many disparate surveillance situations. We argue that the notion of identity is fundamental to surveillance. Rather than having a single identity, individuals have many identities, real and virtual, that are used in different aspects of their lives. Most aspects of life are subject to some form of surveillance, and observations and identities can be aggregated. The notion of identity needs to be theorised. Our analysis is very general and, at the same time, sufficiently precise to be the basis of mathematical models.
△ Less
Submitted 14 August, 2014;
originally announced August 2014.
-
Limits to measurement in experiments governed by algorithms
Authors:
E. J. Beggs,
J. F. Costa,
J. V. Tucker
Abstract:
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 experi…
▽ More
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 in order to 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; we examine its properties in preparation for its use as an oracle. We start to classify 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 with 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.
△ Less
Submitted 19 November, 2009;
originally announced November 2009.
-
Abstract Computability, Algebraic Specification and Initiality
Authors:
J. V. Tucker,
J. I. Zucker
Abstract:
computable functions are defined by abstract finite deterministic algorithms on many-sorted algebras. We show that there exist finite universal algebraic specifications that specify uniquely (up to isomorphism) (i) all abstract computable functions on any many-sorted algebra; and (ii) all functions effectively approximable by abstract computable functions on any metric algebra.
We show that th…
▽ More
computable functions are defined by abstract finite deterministic algorithms on many-sorted algebras. We show that there exist finite universal algebraic specifications that specify uniquely (up to isomorphism) (i) all abstract computable functions on any many-sorted algebra; and (ii) all functions effectively approximable by abstract computable functions on any metric algebra.
We show that there exist universal algebraic specifications for all the classically computable functions on the set R of real numbers. The algebraic specifications used are mainly bounded universal equations and conditional equations. We investigate the initial algebra semantics of these specifications, and derive situations where algebraic specifications define precisely the computable functions.
△ Less
Submitted 2 September, 2001;
originally announced September 2001.
-
Abstract versus Concrete Computation on Metric Partial Algebras
Authors:
J. V. Tucker,
J. I. Zucker
Abstract:
A model of computation is abstract if, when applied to any algebra, the resulting programs for computable functions and sets on that algebra are invariant under isomorphisms, and hence do not depend on a representation for the algebra. Otherwise it is concrete. Intuitively, concrete models depend on the implementation of the algebra.
The difference is particularly striking in the case of topol…
▽ More
A model of computation is abstract if, when applied to any algebra, the resulting programs for computable functions and sets on that algebra are invariant under isomorphisms, and hence do not depend on a representation for the algebra. Otherwise it is concrete. Intuitively, concrete models depend on the implementation of the algebra.
The difference is particularly striking in the case of topological partial algebras, and notably in algebras over the reals. We investigate the relationship between abstract and concrete models of partial metric algebras. In the course of this investigation, interesting aspects of continuity, extensionality and non-determinism are uncovered.
△ Less
Submitted 12 August, 2001;
originally announced August 2001.
