This paper proposes a notion, the 'ambit' of an action, that allows the degree of distribution of an action in a multiagent system to be quantified without regard to its functionality. It demonstrates the use ...
详细信息
ISBN:
(纸本)9780769528564
This paper proposes a notion, the 'ambit' of an action, that allows the degree of distribution of an action in a multiagent system to be quantified without regard to its functionality. It demonstrates the use of that notion in the design, analysis and implementation of dynamically-reconfigurable multi-agent systems. It distinguishes between the extensional (or system) view and intensional (or agent-based) view of such a system and shows how, using the notion of ambit, the step-wise derivation paradigm of Formal Methods can be used to derive the latter from the former In closing it addresses the manner in which these ideas inform studies in the ethics of systems of artificial agents.
This paper attenlpts to provide a formed specification of an Automatic Train Protection (ATP) system. Such a system continuously checks the actual speed of a passenger train against its maximum permitted speed and tak...
详细信息
An overview is given of D-I algebra, an algebra for the specification of the safety and progress properties of delay-insensitive circuits in terms of voltage-level transitions on wires. The algebraic laws make it poss...
详细信息
An overview is given of D-I algebra, an algebra for the specification of the safety and progress properties of delay-insensitive circuits in terms of voltage-level transitions on wires. The algebraic laws make it possible to specify circuits concisely and facilitate the verification of designs. Individual components can be composed into circuits in which signals along internal wires are hidden from the environment. A delay-insensitive approach has been successfully applied to several nontrivial designs, such as the design of a packet router and the design of a constant response-time stack, and D-I algebra has played an important role both in suggesting decompositions and in verifying them.< >
This paper discusses the problem of risk in optimistic simulation protocols, using as example simulation of a distributed mutual exclusion protocol with strong consistency properties. The simulation model is augmented...
ISBN:
(纸本)9780769511047
This paper discusses the problem of risk in optimistic simulation protocols, using as example simulation of a distributed mutual exclusion protocol with strong consistency properties. The simulation model is augmented to detect model inconsistency errors resulting from risky optimistic simulation. While the model runs sequentially without consistency errors, errors occur when the model is executed in parallel optimistically. Some of the errors entirely violate the fundamental mutual exclusion properties of the model itself. To address this problem we extend the optimistic simulation library to eliminate these inconsistencies. We discuss the details of these extensions and the performance trade-off for adding them.
A hybrid architecture for machine vision is described. The primary components of the architecture are a Datacube pipelined image processor, a configurable network of 32 T800 transputers, a Sun-4 workstation and a spec...
详细信息
A hybrid architecture for machine vision is described. The primary components of the architecture are a Datacube pipelined image processor, a configurable network of 32 T800 transputers, a Sun-4 workstation and a special-purpose interface connecting the Datacube to the transputer network. The implementation of a 3D structure-from-motion vision algorithm (Droid) on this architecture is described. This algorithm reconstructs 3D structure by analysing image sequences obtained from a moving camera. The Datacube handles the image digitisation, storage and display; the transputer network performs the feature extraction (corner points) in parallel and the Sun-4 computes the 3D-isation. In this application, which was demonstrated live during a recent ESPRIT conference in Brussels, the architecture delivers a performance of greater than 1 frame per second-17 times the performance of a Sun-4 alone.< >
This paper discusses the problem of risk in optimistic simulation protocols, using as an example, simulation of a distributed mutual exclusion protocol with strong consistency properties. The simulation model is augme...
详细信息
ISBN:
(纸本)076951104X
This paper discusses the problem of risk in optimistic simulation protocols, using as an example, simulation of a distributed mutual exclusion protocol with strong consistency properties. The simulation model is augmented to detect model inconsistency errors resulting from risky optimistic simulation. While the model runs sequentially without consistency errors, errors occur when the model is executed in parallel optimistically. Some of the errors entirely violate the fundamental mutual exclusion properties of the model itself. To address this problem, we extend the optimistic simulation library to eliminate these inconsistencies. We discuss the details of these extensions and the performance tradeoff for adding them.
作者：
Robson, J.M.Oxford University
Programming Research Group Oxford University Computing Laboratory Oxford United Kingdom
Dynamic storage allocation using fixed blocks is usually inefficient in its use of store. The amount of store needed depends on the allocation strategy used. It is proved that for any strategy the amount of store need...
详细信息
A novel process algebra is presented;algebraic expressions specify delay-insensitive circuits in terms of voltage-level transitions on wires. The approach appears to have several advantages over traditional state-grap...
详细信息
Compositional proof systems for shared variable concurrent programs can be devised by including the interference information in the specifications. The formalism falls into a category called rely-guarantee (or assumpt...
详细信息
Compositional proof systems for shared variable concurrent programs can be devised by including the interference information in the specifications. The formalism falls into a category called rely-guarantee (or assumption-commitment), in which a specification is explicitly (syntactically) split into two corresponding parts. This paper summarises existing work on the rely-guarantee method and gives a systematic presentation. A proof system for partial correctness is given first, thereafter it is demonstrated how the relevant rules can be adapted to verify deadlock freedom and convergence. Soundness and completeness, of which the completeness proof is new, are studied with respect to an operational model. We observe that the rely-guarantee method is in a sense a reformulation of the classical non-compositional Owicki & Gries method, and we discuss throughout the paper the connection between these two methods.
暂无评论