Searcharxiv⌕ Search

arXiv subjects

Michael Fisher

Publications and source records attributed to Michael Fisher.

52 records · Page 3Linked to original sources
arXiv2017

The Power of Synchronisation: Formal Analysis of Power Consumption in Networks of Pulse-Coupled Oscillators

We assess the power consumption of network synchronisation protocols, particularly the energy required to synchronise all nodes across a network. We use the widely adopted approach of bio-inspired, pulse-coupled oscillators to achieve network-wide synchronisation and provide an extended formal model of just such a protocol, enhanced with structures for recording energy usage. Exhaustive analysis is then carried out through formal verification, utilising the PRISM model checker to calculate the resources consumed on each possible system execution. This allows us to assess a range of parameter instantiations and to explore trade-offs between power consumption and time to synchronise. This provides a principled basis for the formal analysis of a much broader range of large-scale network protocols.

cs.DC↗
arXiv2017

A Rational Agent Controlling an Autonomous Vehicle: Implementation and Formal Verification

The development and deployment of Autonomous Vehicles (AVs) on our roads is not only realistic in the near future but can also bring significant benefits. In particular, it can potentially solve several problems relating to vehicles and traffic, for instance: (i) possible reduction of traffic congestion, with the consequence of improved fuel economy and reduced driver inactivity; (ii) possible reduction in the number of accidents, assuming that an AV can minimise the human errors that often cause traffic accidents; and (iii) increased ease of parking, especially when one considers the potential for shared AVs. In order to deploy an AV there are significant steps that must be completed in terms of hardware and software. As expected, software components play a key role in the complex AV system and so, at least for safety, we should assess the correctness of these components. In this paper, we are concerned with the high-level software component(s) responsible for the decisions in an AV. We intend to model an AV capable of navigation; obstacle avoidance; obstacle selection (when a crash is unavoidable) and vehicle recovery, etc, using a rational agent. To achieve this, we have established the following stages. First, the agent plans and actions have been implemented within the Gwendolen agent programming language. Second, we have built a simulated automotive environment in the Java language. Third, we have formally specified some of the required agent properties through LTL formulae, which are then formally verified with the AJPF verification tool. Finally, within the MCAPL framework (which comprises all the tools used in previous stages) we have obtained formal verification of our AV agent in terms of its specific behaviours. For example, the agent plans responsible for selecting an obstacle with low potential damage, instead of a higher damage obstacle (when possible) can be formally verified within MCAPL. We must emphasise that the major goal (of our present approach) lies in the formal verification of agent plans, rather than evaluating real-world applications. For this reason we utilised a simple matrix representation concerning the environment used by our agent.

cs.LO↗
arXiv2016

Chromatic Nim finds a game for your solution

We play a variation of Nim on stacks of tokens. Take your favorite increasing sequence of positive integers and color the tokens according to the following rule. Each token on a level that corresponds to a number in the sequence is colored red; if the level does not correspond to a number in the sequence, color it green. Now play Nim on a arbitrary number of stacks with the extra rule: if all top tokens are green, then you can make any move you like. On two stacks, we give explicit characterizations for winning the normal play version for some popular sequences, such as Beatty sequences and the evil numbers corresponding to the 0s in the famous Thue-Morse sequence. We also propose a more general solution which depends only on which of the colors `dominates' the sequence. Our construction resolves a problem posed by Fraenkel at the BIRS 2011 workshop in combinatorial games.

math.CO↗
arXiv2016

Formal Verification of Autonomous Vehicle Platooning

The coordination of multiple autonomous vehicles into convoys or platoons is expected on our highways in the near future. However, before such platoons can be deployed, the new autonomous behaviors of the vehicles in these platoons must be certified. An appropriate representation for vehicle platooning is as a multi-agent system in which each agent captures the "autonomous decisions" carried out by each vehicle. In order to ensure that these autonomous decision-making agents in vehicle platoons never violate safety requirements, we use formal verification. However, as the formal verification technique used to verify the agent code does not scale to the full system and as the global verification technique does not capture the essential verification of autonomous behavior, we use a combination of the two approaches. This mixed strategy allows us to verify safety requirements not only of a model of the system, but of the actual agent code used to program the autonomous vehicles.

cs.AI↗
arXiv2015

Pressure Fluctuations in Natural Gas Networks caused by Gas-Electric Coupling

The development of hydraulic fracturing technology has dramatically increased the supply and lowered the cost of natural gas in the United States, driving an expansion of natural gas-fired generation capacity in several electrical inter-connections. Gas-fired generators have the capability to ramp quickly and are often utilized by grid operators to balance intermittency caused by wind generation. The time-varying output of these generators results in time-varying natural gas consumption rates that impact the pressure and line-pack of the gas network. As gas system operators assume nearly constant gas consumption when estimating pipeline transfer capacity and for planning operations, such fluctuations are a source of risk to their system. Here, we develop a new method to assess this risk. We consider a model of gas networks with consumption modeled through two components: forecasted consumption and small spatio-temporarily varying consumption due to the gas-fired generators being used to balance wind. While the forecasted consumption is globally balanced over longer time scales, the fluctuating consumption causes pressure fluctuations in the gas system to grow diffusively in time with a diffusion rate sensitive to the steady but spatially-inhomogeneous forecasted distribution of mass flow. To motivate our approach, we analyze the effect of fluctuating gas consumption on a model of the Transco gas pipeline that extends from the Gulf of Mexico to the Northeast of the United States.

eess.SY↗
arXiv2015

Towards Verifiably Ethical Robot Behaviour

Ensuring that autonomous systems work ethically is both complex and difficult. However, the idea of having an additional `governor' that assesses options the system has, and prunes them to select the most ethical choices is well understood. Recent work has produced such a governor consisting of a `consequence engine' that assesses the likely future outcomes of actions then applies a Safety/Ethical logic to select actions. Although this is appealing, it is impossible to be certain that the most ethical options are actually taken. In this paper we extend and apply a well-known agent verification approach to our consequence engine, allowing us to verify the correctness of its ethical decision-making.

cs.AI↗
arXiv2014

An Abstract Formal Basis for Digital Crowds

Crowdsourcing, together with its related approaches, has become very popular in recent years. All crowdsourcing processes involve the participation of a digital crowd, a large number of people that access a single Internet platform or shared service. In this paper we explore the possibility of applying formal methods, typically used for the verification of software and hardware systems, in analysing the behaviour of a digital crowd. More precisely, we provide a formal description language for specifying digital crowds. We represent digital crowds in which the agents do not directly communicate with each other. We further show how this specification can provide the basis for sophisticated formal methods, in particular formal verification.

cs.LO↗
arXiv2013

Practical Verification of Decision-Making in Agent-Based Autonomous Systems

We present a verification methodology for analysing the decision-making component in agent-based hybrid systems. Traditionally hybrid automata have been used to both implement and verify such systems, but hybrid automata based modelling, programming and verification techniques scale poorly as the complexity of discrete decision-making increases making them unattractive in situations where complex logical reasoning is required. In the programming of complex systems it has, therefore, become common to separate out logical decision-making into a separate, discrete, component. However, verification techniques have failed to keep pace with this development. We are exploring agent-based logical components and have developed a model checking technique for such components which can then be composed with a separate analysis of the continuous part of the hybrid system. Among other things this allows program model checkers to be used to verify the actual implementation of the decision-making in hybrid autonomous systems.

cs.LO↗
arXiv2010

Proceedings FM-09 Workshop on Formal Methods for Aerospace

The main workshop objective was to promote a holistic view and interdisciplinary methods for design, verification and co-ordination of aerospace systems, by combining formal methods with techniques from control engineering and artificial intelligence. The very demanding safety, robustness and performance requirements of these systems require unprecedented integration of heterogeneous techniques and models. The aim of FMA was to bring together active researchers from all the above areas to discuss and present their work.

cs.LO↗
arXiv2010

Agent Based Approaches to Engineering Autonomous Space Software

Current approaches to the engineering of space software such as satellite control systems are based around the development of feedback controllers using packages such as MatLab's Simulink toolbox. These provide powerful tools for engineering real time systems that adapt to changes in the environment but are limited when the controller itself needs to be adapted. We are investigating ways in which ideas from temporal logics and agent programming can be integrated with the use of such control systems to provide a more powerful layer of autonomous decision making. This paper will discuss our initial approaches to the engineering of such systems.

cs.MA↗
arXiv2007

Radiation Pressure in Lyman-alpha Forest Clouds

The effective recombination coefficient, alpha_eff, is refined for optically thin cases. Radiation pressure in Lyman-alpha and HeII Lyman-alpha is calculated in terms of the number density and the mean free path. Pressure equilibrium between Lyman-alpha clouds and an adiabatically expanding inter-galactic medium is assumed, n_i T_i = n_c T_c. Numerical models of isothermal and adiabatic expanding Lyman-alpha forest clouds are presented, including evolving UV sources (QSOs), with various turn-on times z_on = 20, 10, and 5, and with q_0 = 1/2 in a matter-dominated Friedmann-Robertson-Walker Universe. These models lead to the conclusion that the radiation pressure and QSO turn-on time are significant in determining the range of physical size, D, and neutral hydrogen column density, N(HI), permitted for stable Lyman-alpha forest clouds. This manuscript was written in 1989 and never submitted for publication.

astro-ph↗
arXiv2007

The Hot Inter-Galactic Medium and the Cosmic Microwave Background

The physical characteristics of the Lyman-alpha forest cloud systems are combined with observations on the baryonic mass density of the Universe and constraints from primordial nucleosynthesis to set boundary conditions on the Intergalactic Medium (IGM) at the epoch of z=2.5. The Universe is considered a closed system and allowed to expand adiabatically from the epoch when QSOs first ionized the IGM (5 <= z_on <= 20). The average kinetic energy of a gas is calculated in the region where the gas transitions from relativistic to non-relativistic behavior. All of the above measurements are then used to determine the thermal history of the IGM in the redshift range 2.5 <= z <= z_on. The hot IGM is assumed to inverse Compton scatter photons from the Cosmic Microwave Background (CMBR) and consequently distort the CMBR as seen at the present epoch. The temperature of the IGM at z=2.5 and the epoch z_on are adjusted, within the constraints defined above, to give the best overall agreement with published data on the temperature of the IGM. We find that the model of the IGM proposed here does not grossly distort the CMBR, and in fact agrees quite closely with the preliminary results from the Cosmic Background Explorer (COBE) satellite. However, our model of the IGM cannot explain the observed cosmic x ray background. This paper was originally written in 1990. It was never submitted for publication.

astro-ph↗
arXiv2007

Efficient First-Order Temporal Logic for Infinite-State Systems

In this paper we consider the specification and verification of infinite-state systems using temporal logic. In particular, we describe parameterised systems using a new variety of first-order temporal logic that is both powerful enough for this form of specification and tractable enough for practical deductive verification. Importantly, the power of the temporal language allows us to describe (and verify) asynchronous systems, communication delays and more complex properties such as liveness and fairness properties. These aspects appear difficult for many other approaches to infinite-state verification.

cs.LO↗
arXiv2003

Monodic temporal resolution

Until recently, First-Order Temporal Logic (FOTL) has been little understood. While it is well known that the full logic has no finite axiomatisation, a more detailed analysis of fragments of the logic was not previously available. However, a breakthrough by Hodkinson et.al., identifying a finitely axiomatisable fragment, termed the monodic fragment, has led to improved understanding of FOTL. Yet, in order to utilise these theoretical advances, it is important to have appropriate proof techniques for the monodic fragment. In this paper, we modify and extend the clausal temporal resolution technique, originally developed for propositional temporal logics, to enable its use in such monodic fragments. We develop a specific normal form for formulae in FOTL, and provide a complete resolution calculus for formulae in this form. Not only is this clausal resolution technique useful as a practical proof technique for certain monodic classes, but the use of this approach provides us with increased understanding of the monodic fragment. In particular, we here show how several features of monodic FOTL are established as corollaries of the completeness result for the clausal temporal resolution method. These include definitions of new decidable monodic classes, simplification of existing monodic classes by reductions, and completeness of clausal temporal resolution in the case of monodic logics with expanding domains, a case with much significance in both theory and practice.

cs.LO↗
arXiv2000

Clausal Temporal Resolution

In this article, we examine how clausal resolution can be applied to a specific, but widely used, non-classical logic, namely discrete linear temporal logic. Thus, we first define a normal form for temporal formulae and show how arbitrary temporal formulae can be translated into the normal form, while preserving satisfiability. We then introduce novel resolution rules that can be applied to formulae in this normal form, provide a range of examples and examine the correctness and complexity of this approach is examined and. This clausal resolution approach. Finally, we describe related work and future developments concerning this work.

cs.LO↗