The publications tab on the webpage here is more up-to-date.
A Discipline of Mathematical Systems Modelling
Matthew Collinson, Brian Monahan and David Pym.
College
Publications, March 2012. ISBN-13: 978-1-904987-50-5.
Preface. The mathematization of the sciences, of engineering, and of economics has been an outstandingly successful intellectual enterprise, enabling the modern world. As the operations of the world become more and more dependent on highly interconnected, massively complex, networked systems of computational devices, the need to develop a mathematical understanding of their properties and behaviours is increasingly pressing.
Our approach, described in this monograph, is to combine the compositionality of formal specification --- using techniques from algebra, computation theory, logic, and probability theory --- with the control of level of abstraction afforded by the classical mathematical modelling method.
The first chapter provides a complete high-level view of the approach to systems modelling that is developed in the monograph. It provides both conceptual and philosophical background and introductions to the technical development. The remaining chapters develop the mathematical and computational aspects of our approach. Each chapter develops a specific mathematical or computational component, clearly integrated into the overall development. Examples, including ones based on industrial and commercial applications, are provided throughout. An implementation of a simulation engine (Core Gnosis) for executing models is available for download from HP Labs. Associated with this monograph is a website (http://www.hpl.hp.com/research/systems_security/gnosis.html) from which Core Gnosis may be obtained. This is book is about the conceptual and mathematical foundations of a modelling approach, with indications of how it can, and has been, deployed in practice. We defer to another occasion an account of the pragmatics of the deployment.
Gnosis
A package including the Gnosis simulation system and the LSCRP/MBI model-checker
discussed in the `Discipline' book is available from Hewlett-Packard Laboratories
here.
Duality and Decision.
Working manuscript. Current upload version: 20th Sept. 2012.
A short note on the potential application of topological duality in decision theory.
Draft
here.
A Substructural Logic for Layered Graphs.
Matthew Collinson, Kevin McDonald and David Pym.
Submitted to journal.
Abstract. Complex systems, be they natural or synthetic, are ubiquitous. In particular, complex networks of devices and services underpin most of society's operations. By their very nature, such systems are difficult to conceptualize and reason about effectively. The concept of layering is widespread in complex systems, but has not been considered conceptually. Noting that graphs are a key formalism in the description of complex systems, we establish a notion of a layered graph. We provide a logical characterization of this notion of layering using a non-associative, non-commutative substructural, separating logic. We provide soundness and completeness results for a class of algebraic models that includes layered graphs, which give a mathematically substantial semantics to this very weak logic. We explain, via examples, applications in information processing and security.
Draft here.
Trust Domains: An Algebraic, Logical, and Utility-theoretic Approach.
Gabrielle Anderson, Matthew Collinson and David Pym.
In Proc. TRUST 2013, and
Trust and Trustworthy Computing,
M. Huth, N. Asokan, S. Capkun, I. Flechais, L. Coles-Kemp (editors),
Springer LNCS 7904, 2013.
Draft here.
Utility-based Decision-making in Distributed Systems Modelling
[Extended Abstract].
Gabrielle Anderson, Matthew Collinson and David Pym.
In Proc. Theoretical Aspects of Reasoning about Knowledge (TARK) 2013,
Burkhard C. Schipper (editor), Chennai, 2013. ISBN: 978-0-615-74716-3.
Available on the Computing Research Repository
(CoRR).
Abstract. We consider a calculus of resources and processes as a basis for modelling decision-making in multi-agent systems. The calculus represents the regulation of agents' choices using utility functions that take account of context. Associated with the calculus is a (Hennessy-Milner-style) context-sensitive modal logic of state. As an application, we show how a notion of `trust domain' can be defined for multi-agent systems.
Draft here.
A Framework for Modelling Security Architectures in Services
Ecosystems.
Matthew Collinson, David Pym and Barry Taylor.
In Proc. ESOCC 2012.
LNCS: 7592, 64-79, 2012.
Semantics for Structured Systems Modelling and Simulation.
Matthew Collinson, Brian Monahan and David Pym.
Proc. Simutools 2010,
ACM Digital Library and EU Digital Library.
ISBN: 78-963-9799-87-5.
Abstract. Simulation modelling is an important tool for exploring and reasoning about the dynamics and properties of complex systems, and many supporting languages are available. Commonly occurring features of these languages are constructs that capture concepts such as process, resource, and location. We describe a mathematical framework that supports a modelling idiom based on these core concepts, and which also adopts stochastic methods for representing the environments within which systems exist. We explain how this framework can be used to give a formal semantics to a simulation modelling language, Core Gnosis, that includes basic constructs for process, resource, and location. We include a brief discussion of a system of logic for reasoning about our models that is compositional with respect to the structure of models. We believe that our mathematical analysis of systems in terms of process, resource, location, and stochastic environment, together with a language that captures these concepts quite directly, leads to an efficient and robust modelling framework within which natural mathematical reasoning about systems is captured in the associated tools.
Algebra and Logic for Access Control.
Matthew Collinson and David Pym. Formal Aspects of Computing 22 (2), 83-104,
2010.
Erratum: Formal
Aspects of Computing 22 (3-4), 483-484, 2010.
Abstract. The access control problem in computer security is fundamentally concerned with the ability of system entitites to see, make use of, or alter various system resources. As such, many access control situations are essentially problems of concurrency. We give an account of fundamental situations in access-control in distributed systems using a resource-based process calculus and a hybrid of Hennessy-Milner and resource logic. This yields a consistent account of operational behaviour and logical reasoning for access control, that includes an analysis of co-signing, roles and chains-of-trust.
The original publication is available at http://www.springerlink.com. An HP Labs Technical Report (with erratum incorporated) as HPL-2008-75R1.
Algebra and Logic for Resource-based Systems Modelling.
Matthew Collinson wand David Pym.
Mathematical Structures in Computer Science
19:959-1027, 2009. doi:10.1017/S0960129509990077.
Abstract. Mathematical modelling is one of the fundamental tools of science and engineering. Very often, models are required to be executable, as a simulation, on a computer. In this paper, we present some contributions to the process-theoretic and logical foundations of discrete-event modelling with resources and processes. We present a process calculus with an explicit representation of resources in which processes and resources co-evolve. The calculus is closely connected to a logic that may be used as a specification language for properties of models. The logic is strong enough to allow requirements that a system have certain structure; for example, that it is a parallel composite of subsystems. This work consolidates, extends, and improves upon aspects of the earlier works. An extended example, consisting of a semantics for a simple parallel programming language, indicates a connection with separating logics for concurrency.
Erratum: Page 994 (page 36 in the preprint), Fig. 7: in each of the bottom two clauses, R , E ~ R , vS.F should be E ~ vS.F
Draft here
A Logical and Computational Theory of Located Resource.
Matthew Collinson, Brian Monahan and David Pym.
Journal of Logic and Computation 19 (b): 1207-1244, 2009.
Advance Access published on 22 July, 2009. doi:10.1093/logcom/exp021.
Also available as an HP Labs Technical Report: HPL-2008-74R1.
Abstract. Experience of practical systems modelling suggests that the key conceptual components of a model of a system are processes, resources, locations, and environment. In recent work, we have given a process-theoretic account of this view in which resources as well as processes are first-class citizens. This process calculus, SCRP, captures the structural aspects of the semantics of the Demos2k modelling tool. Demos2k represents environment stochastically using a wide range of probability distributions and queue-like data structures. Associated with SCRP is a (bunched) modal logic, MBI, which combines the usual additive connectives of Hennessy-Milner logic with their multiplicative counterparts. In this paper, we complete our conceptual framework by adding to SCRP and MBI an account of a notion of location that is simple yet sufficiently expressive to capture naturally a wide range of forms of location, both spatial and logical. We also provide a sketch of an extension of the Demos2k tool to incorporate this notion of location.
An Update to Located Demos2k.
Matthew Collinson, Brian Monahan and David Pym. 2008.
Available as an HP Labs Technical Report:
HPL-2008-205.
Abstract. We give here a short update concerning Located Demos2k briefly describing the ability to forget and recall resource links, as reported in an earlier Technical Report. We also briefly mention our (purely applicative) implementation in OCaml of a simulator for Located Demos2k. Two appendices contain a substantial example of Located Demos2k, presented in OCaml terms, and the execution trace produced by the implementation.
Located Demos2k: A Tool for Executing Processes Relative to
Distributed Resources.
Matthew Collinson, Brian Monahan and David Pym. 2008.
Available as an HP Labs Technical Report:
HPL-2008-76
Abstract. We describe the background to, and the current state of the development of, Located Demos2k, an executable modelling language which reconstructs the Demos2k language starting from an explicit model of location. The version of Located Demos2k described herein is the first useful stage in its development, and provides convenient a point of departure of discussing its further development.
Unfinished below this point ... sorry.
Erratum to Pym Tofts papers
MFPS paper on applications of Bunched Poly
Bunched Polymorphism.
Matthew Collinson, David Pym and Edmund Robinson.
Mathematical Structures in Computer Science 18(6),
1091-1132, 2008. doi: 10.1017/S0960129508007159.
Abstract. We describe a polymorphic, typed lambda calculus with substructural features. This calculus extends the first-order substructural lambda calculus alpha-lambda associated with bunched logic. A particular novelty of our new calculus is the substructural treatment of second-order variables. This is accomplished through the use of bunches of type variables in typing contexts. Both additive and multiplicative forms of polymorphic abstraction are then supported. The calculus has sensible proof-theoretic properties and a straightforward categorical semantics using indexed categories. We produce a model for additive polymorphism with first-order bunching based on partial equivalence relations. We consider additive and multiplicative existential quantifiers separately from the universal quantifiers.
Draft here.
Bunched Poly: CSL extented abstract
Older stuff
Topological Transition Structures
Modal Duality Conference paper. International Conference on Non-Classical Logics website
PhD Thesis
Manchester Tech Report
MSc Thesis