Commutative regular expressions describe sets of unordered words, and are used, for example, when building type systems for process calculi. In these applications, an important operation is finding the intersection of two expressions, but no algorithm currently exists. We remedy this by proposing an algorithm for computing intersections of commutative regular expressions, which we implement and prove correct in the Rocq prover. The algorithm encodes the intersection of two expressions as systems of linear Diophantine equations, and extracts from their solution an intersection expression. To solve these systems we implement and verify the algorithm proposed by Contejean and Devie. We detail the implementation of the intersection algorithm, highlight essential aspects of the proofs (including the complex proof of termination of the equation system solver), and evaluate the OCaml-extracted solver on random and real-world commutative regular expressions.

Resource Description Framework (RDF) is a widespread W3C standard defining a domain-specific language for knowledge representation, providing a platform to build higher-level languages such as OWL or SHACL. RDF concrete syntaxes define an external representation of its abstract model for data interchange. Despite sharing the same core semantics, RDF concrete syntaxes differ in how well they support common modelling idioms at the surface level. Many RDF libraries have been implemented in Scheme, however, they support few concrete syntaxes and/or do not exhibit compliance with the W3C test suites.

Abstract With many governments regulating the handling of user data—the General Data Protection Regulation, the California Consumer Privacy Act, and the Saudi Arabian Personal Data Protection Law—ensuring systems comply with data privacy legislation is of high importance. Checking compliance is a tricky process and often includes many manual elements. We propose that formal methods, that model systems mathematically, can provide strong guarantees to help companies prove their adherence to legislation. To increase usability we advocate a diagrammatic approach, based on bigraphical reactive systems, where privacy experts can explicitly visualise the systems and describe updates, via rewrite rules, that describe system behaviour. The rewrite rules allow flexibility in integrating privacy policies with user-specified systems. We focus on modelling notions of providing consent, withdrawing consent, purpose limitations, the right to access and sharing data with third parties , and define privacy properties that we want to prove within the systems. Properties are expressed using the computation tree logic and proved using model checking. To show the generality of the proposed framework, we apply it to two examples: a bank notification system, inspired by Monzo’s privacy policy, and a cloud-based home healthcare system based on the Fitbit app’s privacy policy.

Bigraphs are a versatile modelling formalism that allows easy expression of placement and connectivity relations in a graphical format. System evolution is user defined as a set of rewrite rules. This article presents a practical, yet detailed guide to developing, executing, and reasoning about bigraph models, including recent extensions such as parameterised, instantaneous, prioritised and conditional rules, and probabilistic and stochastic rewriting.

Belief-Desire-Intention (BDI) agents feature uncertain beliefs (e.g. sensor noise), probabilistic action outcomes (e.g. attempting and action and failing), and non-deterministic choices (e.g. what plan to execute next). To be safely applied in real-world scenarios we need reason about such agents, for example, we need probabilities of mission success and the strategies used to maximise this. Most agents do not currently consider uncertain beliefs, instead a belief either holds or does not. We show how to use epistemic states to model uncertain beliefs, and define a Markov Decision Process for the semantics of the Conceptual Agent Notation (Can) agent language allowing support for uncertain beliefs, non-deterministic event, plan, and intention selection, and probabilistic action outcomes. The model is executable using an automated tool—CAN-verify—that supports error checking, agent simulation, and exhaustive exploration via an encoding to Bigraphs that produces transition systems for probabilistic model checkers such as PRISM. These model checkers allow reasoning over quantitative properties and strategy synthesis. Using the example of an autonomous submarine and drone surveillance together with scalability experiments, we demonstrate our approach supports uncertain belief modelling, quantitative model checking, and strategy synthesis in practice.

We present CAN-Verify , an automated tool for analysing BDI agents written in the Conceptual Agent Notation ( Can ) language. CAN-Verify includes support for syntactic error detection before agent execution, agent program interpretation (running agents), and model-checking of agent programs (analysing agents). The model checking supports verifying the correctness of agents against both generic agent requirements, such as if a task is accomplished, and user-defined requirements, such as certain beliefs eventually holding. The latter can be expressed in structured natural language, allowing the tool to be used by agent programmers without formal training in the underlying verification techniques.

Formal Modelling is often used as part of the design and testing process of software development to ensure that components operate within suitable bounds even in unexpected circumstances. We conducted a user study evaluation of predictive formal modelling (PFM) at runtime in a human-swarm mission to determine the benefit of PFM on performance and human-swarm interaction. A total of 180 participants were recruited to perform the role of aerial swarm operators delivering parcels to target locations in a simulation environment. The PFM model was integrated into the simulation software to inform the operator of the estimated mission completion time given the current number of drones deployed. The operator could increase the number of parcels delivered in any timestep by adding drones, which also increased costs, thus requiring the use of the minimum number of drones necessary to complete the task in the given time. We collected user feedback using standard survey questionnaires and measured performance using data obtained from the Human and Robot Interactive Swarm (HARIS) simulator. Our results show that PFM increased the performance of the human swarm team without significantly increasing the operators’ workload or affecting the system’s usability.

As more end-user applications depend on Internet of Things (IoT) technology, it is essential the networking protocols underpinning these applications are reliable. Using Formal Methods to reason about protocol specifications is an established technique, but, due to their perceived difficulty and mathematical nature, receive limited use in practice. We propose an approach based on Milner’s bigraphs—a flexible diagrammatic modelling language—that allows developers to “draw” the protocol updates as a way to increase use of formal methods in protocol design. To show bigraphs in action, we model part of the Routing Protocol for low-power and Lossy Networks (RPL), popular in wireless sensor networks, and verify it using model checking. We compare our approach with the more common simulation approach and show that analysing the bigraph model often finds more valid routes than simulation (which usually returns only a single routing tree even with 500 simulations) and that it has comparable performance. The model is open to extension, with less implementation effort than simulation, and we show this through two examples: a security attack and physical link drops. Bigraphs seem a promising approach to protocol design, and this is the first step in promoting their use.

Abstract Belief–desire–intention (BDI) agents are a popular agent architecture. We extend conceptual agent notation (Can)—a BDI programming language with advanced features such as failure recovery and declarative goals—to include probabilistic action outcomes, e.g. to reflect failed actuators, and probabilistic policies, e.g. for probabilistic plan and intention selection. The extension is encoded in Milner’s bigraphs. Through application of our BigraphER tool and the PRISM model checker, theprobabilityof success (intention completion) under different probabilistic outcomes and plan/event/intention selection strategies can be investigated and compared. We present a smart manufacturing use case. A significant result is that plan selection has limited effect compared with intention selection. We also see that the impact of action failures can be marginal—even when failure probabilities are large—due to the agent making smarter choices.

Robot swarms, through redundancy, offer fault-tolerant distributed sensing and actuation, but can lack complex mission-level decision making. Pairing a human operator with the swarm can improve decision making but only if the operator maintains situational awareness—knowledge of the current state of the swarm—as well as being able to anticipate future states. We show how formal methods, in the form of probabilistic models, executed and verified at runtime alongside the system can aid situational awareness by providing valuable insight into both current and future situations. Two models, for determining task and mission success probabilities, are given, and we show that statistical model checking allows timely approximate predictions that take no more than 1s while staying within 2% of the exact solution. We highlight and implement approaches to display this information to an operator, and show how models can be used to try what-if scenarios before decisions are made.

The Belief-Desire-Intention (BDI) architecture is a popular framework for rational agents, yet most verification approaches are limited to analysing the behaviours of an agent in a subset of all possible environments.However, in practice, BDI agents operate in dynamic environments where the exact occurrence of external changes is difficult to predict.For safety/security we need to assess whether the agent behaves as required in all circumstances.To address this, we define environments, accounting for both sensor information about physical changes and new tasks to be completed, as a non-deterministic finitestate automata.We give an environment-enabled extension to the Conceptual Agent Notation (CAN) language including an executable semantics via an encoding to Milner's bigraphs and the BigraphER tool.We illustrate the framework through a simple Unmanned Aerial Vehicle (UAV) example that is verified using mainstream tools including PRISM model checker.Results show our approach can automatically identify agent design flaws to aid agent programmers in design, debugging, and analysis.

Bigraphs are a universal computational modelling formalism for the spatial and temporal evolution of a system in which entities can be added and removed. We extend bigraphs to probabilistic bigraphs, and then again to action bigraphs, which include non-determinism and rewards. The extensions are implemented in the BigraphER toolkit and illustrated through examples of virus spread in computer networks and data harvesting in wireless sensor systems. BigraphER also supports the existing stochastic bigraphs extension of Krivine et al. and using BigraphER we give, for the first time, a direct implementation of the membrane budding model used to motivate stochastic bigraphs.

Electric vehicles (EVs) are increasingly becoming an environmental-friendly option in current transportation systems, thanks to reduced fossil fuel consumption and carbon emission. However, the more widespread adoption of EVs has been hampered by following two factors: the lack of charging infrastructure and the limited cruising range. Energy consumption estimation is crucial to address these challenges as it provides the foundations to enhance charging-station deployment, improve eco-driving behavior, and extend the EV cruising range. In this article, we propose an EV energy consumption estimation method capable of achieving accurate estimation despite insufficient EV data and ragged driving trajectories. It consists of following three distinct features: knowledge transfer from internal combustion engine/hybrid electric vehicles to EVs, segmentation-aided trajectory granularity, time-series estimation based on bidirectional recurrent neural network. Experimental evaluation shows our method outperforms other machine learning benchmark methods in estimating energy consumption on a real-world vehicle energy dataset.

Bigraphs simultaneously model the spatial and non-spatial relationships between entities, and have been used for systems modelling in areas including biology, networking, and sensors. Temporal evolution can be modelled through a rewriting system, driven by a matching algorithm that identifies instances of bigraphs to be rewritten. The previous state-of-the-art matching algorithm for bigraphs with sharing is based on Boolean satisfiability (SAT), and suffers from a large encoding that limits scalability and makes it hard to support extensions. This work instead adapts a subgraph isomorphism solver that is based upon constraint programming to solve the bigraph matching problem. This approach continues to support bigraphs with sharing, is more open to other extensions and side constraints, and improves performance by over two orders of magnitude on a range of problem instances drawn from real-world mixed-reality, protocol, and conference models.

This paper analyses models of a spatial logic with path operators based on the class of neighbourhood spaces, also called pretopological or closure spaces, a generalisation of topological spaces. For this purpose, we distinguish two dimensions: the type of spaces on which models are built, and the type of allowed paths. For the spaces, we investigate general neighbourhood spaces and the subclass of quasi-discrete spaces, which closely resemble graphs. For the paths, we analyse the cases of quasi-discrete paths, which consist of an enumeration of points, and topological paths, based on the unit interval. We show that the logic admits finite models over quasi-discrete spaces, both with quasi-discrete and topological paths. Finally, we prove that for general neighbourhood spaces, the logic does not have the finite model property, either for quasi-discrete or topological paths.

Abstract Designing and reasoning about complex systems such as wireless sensor networks is hard due to highly dynamic environments: sensors are heterogeneous, battery-powered, and mobile. While formal modelling can provide rigorous mechanisms for design/reasoning, they are often viewed as difficult to use. Graph rewrite-based modelling techniques increase usability by providing an intuitive, flexible, and diagrammatic form of modelling in which graph-like structures express relationships between entities while rewriting mechanisms allow model evolution. Two major graph-based formalisms are Graph Transformation Systems (GTS) and Bigraphical Reactive Systems (BRS). While both use similar underlying structures, how they are employed in modelling is quite different. To gain a deeper understanding of GTS and BRS, and to guide future modelling, theory, and tool development, in this experience report we compare the practical modelling abilities and style of GTS and BRS when applied to topology control in WSNs. To show the value of the models, we describe how analysis may be performed in both formalisms. A comparison of the approaches shows that although the two formalisms are different, from both a theoretical and practical modelling standpoint, they are each successful in modelling topology control in WSNs. We found that GTS, while featuring a small set of entities and transformation rules, relied on entity attributes, rule application based on attribute/variable side-conditions, and imperative control flow units. BRS on the other hand, required a larger number of entities in order to both encode attributes directly in the model (via nesting) and provide tagging functionality that, when coupled with rule priorities, implements control flow. There remains promising research mapping techniques between the formalisms to further enable flexible and expressive modelling.

We present a bisimulation relation for neighbourhood spaces, a generalisation of topological spaces. We show that this notion, path preserving bisimulation, preserves formulas of the spatial logic SLCS. We then use this preservation result to show that SLCS cannot express standard topological properties such as separation and connectedness. Furthermore, we compare the bisimulation relation with standard modal bisimulation and modal bisimulation with converse on graphs and prove it coincides with the latter.

Graphical Internet of Things (IoT) device management platforms, such as IoTtalk, make it easy to describe interactions between IoT devices. Applications are defined by dragging-and-dropping devices and specifying how they are connected, e.g., a door sensor controlling a light. While this allows simple and rapid development, it remains possible to specify unwanted device configurations, such as using the same device to drive a motor up and down simultaneously, risking damaging the motor. We propose BigraphTalk, a verification framework for IoTtalk that utilizes formal techniques, based on bigraphs, to statically guarantee that unwanted configurations do not arise. In particular, we check for invalid connections between devices, as well as type errors, e.g., passing a float to a Boolean switch. To the best of our knowledge, BigraphTalk is the first platform to support the graphical specification of correct-by-design IoT applications. BigraphTalk provides fully automated verification and feedback without end-users ever needing to specify a bigraph. This means that any application, specifiable in IoTtalk, is guaranteed, so long as verification succeeds, not to violate the given configuration constraints when deployed; with no extra cost to the user.

When a component fails in a critical communications service, how urgent is a repair? If we repair within 1 hour, 2 hours, or$n$hours, how does this affect the likelihood of service failure? Can a formal model support assessing the impact, prioritisation, and scheduling of repairs in the event of component failures, and forecasting of maintenance costs? These are some of the questions posed to us by a large organisation and here we report on our experience of developing a stochastic framework based on a discrete space model and temporal logic to answer them. We define and explore both standard steady-state and transient temporal logic properties concerning the likelihood of service failure within certain time bounds, forecasting maintenance costs, and we introduce a new concept ofenvelopes of behaviourthat quantify the effect of the status of lower level components on service availability. The resulting model is highly parameterised and user interaction for experimentation is supported by a lightweight, web-based interface.

Large-scale wireless sensor networks (WSN) are increasingly deployed and an open question is how they can support multiple applications. Networks and sensing devices are typically heterogeneous and evolving: topologies change, nodes drop in and out of the network, and devices are reconfigured. The key question we address is how to verify that application requirements are met, individually and collectively, and can continue to be met, in the context of large-scale, evolving network and device configurations. We define a modelling and verification framework based on Bigraphical Reactive Systems (BRS) for modelling, with bigraph patterns and temporal logic properties for specifying application requirements. The bigraph diagrammatic notation provides an intuitive representation of concepts such as hierarchies, communication, events and spatial relationships, which are fundamental to WSNs. We demonstrate modelling and verification through a real-life urban environmental monitoring case-study. A novel contribution is automated online verification using BigraphER and replay of real-life sensed data streams and network events by the Cooja network simulator. Performance results for verification of two application properties running on a WSN with up to 200 nodes indicate our framework is capable of handling WSNs of that scale.

While HCI has a long tradition of formally modelling task-based interactions with graphical user interfaces, there has been less progress in modelling emerging ubiquitous computing systems due in large part to their highly contextual nature and dependence on unreliable sensing systems. We present an exploration of modelling an example ubiquitous system, the Savannah game, using the mathematical formalism of bigraphs, which are based on a universal process algebra that encapsulates both dynamic and spatial behaviour of autonomous agents that interact and move among each other, or within each other. We establish a modelling approach based on four perspectives on ubiquitous systems—Computational, Physical, Human, and Technology—and explore how these interact with one another. We show how our model explains observed inconsistencies in user trials of Savannah, and then, how formal analysis reveals an incompleteness in design and guides extensions of the model and/or possible system re-design to resolve this.

Bigraphical Reactive Systems (BRS) were designed by Milner as a universal formalism for modelling systems that evolve in time, locality, co-locality and connectivity. But the underlying model of location (the place graph) is a forest, which means there is no straightforward representation of locations that can overlap or intersect. This occurs in many domains, for example in wireless signalling, social interactions and audio communications. Here, we define bigraphs with sharing, which solves this problem by an extension of the basic formalism: we define the place graph as a directed acyclic graph, thus allowing a natural representation of overlapping or intersecting locations. We give a complete presentation of the theory of bigraphs with sharing, including a categorical semantics, algebraic properties, and several essential procedures for computation: bigraph with sharing matching, a SAT encoding of matching, and checking a fragment of the logic BiLog. We show that matching is an instance of the NP-complete sub-graph isomorphism problem and our approach based on a SAT encoding is also efficient for standard bigraphs. We give an overview of BigraphER (Bigraph Evaluator & Rewriting), an efficient implementation of bigraphs with sharing that provides manipulation, simulation and visualisation. The matching engine is based on the SAT encoding of the matching algorithm. Examples from the 802.11 CSMA/CA RTS/CTS protocol and a network management support system illustrate the applicability of the new theory.

Abstract Stochastic bigraphical reactive systems (SBRS) is a recent formalism for modelling systems that evolve in time and space. However, the underlying spatial model is based on sets of trees and thus cannot represent spatial locations that are shared among several entities in a simple or intuitive way. We adopt an extension of the formalism, SBRS with sharing , in which the topology is modelled by a directed acyclic graph structure. We give an overview of SBRS with sharing, we extend it with rule priorities, and then use it to develop a model of the 802.11 CSMA/CA RTS/CTS protocol with exponential backoff, for an arbitrary network topology with possibly overlapping signals. The model uses sharing to model overlapping connectedness areas, instantaneous prioritised rules for deterministic computations, and stochastic rules with exponential reaction rates to model constant and uniformly distributed timeouts and constant transmission times. Equivalence classes of model states modulo instantaneous reactions yield states in a CTMC that can be analysed using the model checker PRISM. We illustrate the model on a simple example wireless network with three overlapping signals and we present some example quantitative properties.

Home wireless networks are difficult to manage and comprehend because of evolving locality, co-locality, connectivity and interaction. We define formal models of home wireless network infrastructure and policies and investigate how they can be used in a network management system designed to provide user-oriented support. We model spatial and temporal behaviour of network interactions and user-initiated network policies and define an online framework for generation of models from network and user-initiated events. The models are expressed in an extension to Milnerʼs bigraphical reactive systems. Analysis of the models is carried out in real-time by a bespoke bigraph reasoning system based on checking predicates, which is encoded as bigraph matching. Real-time model generation and analysis is implemented on the experimental Homework system router and trialled with synthetic and actual network data.