Model checking for a probabilistic branching time logic with fairness

We consider concurrent probabilistic systems, based on probabilistic automata of Segala & Lynch [55], which allow non-deterministic choice between probability distributions. These systems can be decomposed into a collection of “computation trees” which arise by resolving the non-deterministic, but not probabilistic, choices. The presence of non-determinism means that certain liveness properties cannot be established unless fairness is assumed. We introduce a probabilistic branching time logic PBTL, based on the logic TPCTL of Hansson [30] and the logic PCTL of [55], resp. pCTL [14]. The formulas of the logic express properties such as “every request is eventually granted with probability at least p”. We give three interpretations for PBTL on concurrent probabilistic processes: the first is standard, while in the remaining two interpretations the branching time quantifiers are taken to range over a certain kind of fair computation trees. We then present a model checking algorithm for verifying whether a concurrent probabilistic process satisfies a PBTL formula assuming fairness constraints. We also propose adaptations of existing model checking algorithms for pCTL [4, 14] to obtain procedures for PBTL under fairness constraints. The techniques developed in this paper have applications in automatic verification of randomized distributed systems. Received: June 1997 / Accepted: May 1998     

A hybrid system approach for supporting digital libraries

A digital library (DL) consists of a database which contains library information and a user interface which provides a visual window for users to search relevant information stored in the database. Thus, an abstract structure of a digital library can be defined as a combination of a special purpose database and a user-friendly interface. This paper addresses one of the fundamental aspects of such a combination. This is the formal data structure for linking an object oriented database with hypermedia to support digital libraries. It is important to establish a formal structure for a digital library in order to efficiently maintain different types of library information. This article discusses how to build an object oriented hybrid system to support digital libraries. In particular, we focus on the discussion of a general purpose data model for digital libraries and the design of the corresponding hypermedia interface. The significant features of this research are, first, a formalized data model to define a digital library system structure; second, a practical approach to manage the global schema of a library system; and finally, a design strategy to integrate hypermedia with databases to support a wide range of application areas. Received: 15 December 1997 / Revised: June 1999     

Creating word-level language models for large-vocabulary handwriting recognition

We discuss development of a word-unigram language model for online handwriting recognition. First, we tokenize a text corpus into words, contrasting with tokenization methods designed for other purposes. Second, we select for our model a subset of the words found, discussing deviations from an N-most-frequent-words approach. From a 600-million-word corpus, we generated a 53,000-word model which eliminates 45% of word-recognition errors made by a character-level-model baseline system. We anticipate that our methods will be applicable to offline recognition as well, and to some extent to other recognizers, such as speech recognizers and video retrieval systems. Received: November 1, 2001 / Revised version: July 22, 2002     

The level of handshake required for managing a connection

A connection between two hosts across a wide-area network may consist of many sessions over time, each called an incarnation. A connection is synchronized using a connection establishment protocol, based on a handshake mechanism, to allow reliable exchange of data. This paper identifies the precise level of handshake needed under different assumptions on the nodes and on the network, using a formal model for connection management. In particular, the following parameters are studied: the size of the memory at the nodes, the information retained between incarnations, and the existence of time constraints on the network. Among the results we obtain are: (1) If both nodes have bounded memory, no incarnation management protocol exists. (2) If the nodes have unbounded memory, then a two-way handshake incarnation management protocol exists. (3) If the nodes have unbounded memory, and the server does not retain connection-specific information between incarnations, then a three-way handshake incarnation management protocol exists. On the other hand, a two-way handshake incarnation management protocol does not exist, even if some global information is retained. (4) If a bound on maximum packet lifetime (MPL) is known, then a two-way handshake incarnation management protocol exists, in which the server does not retain connection-specific information between incarnations. Received: July 1995 / Accepted: July 1997     

Drag-and-drop multimedia: ¶an interface framework for digital libraries

In this paper, we describe a new interface for querying multimedia digital libraries and an interface building framework. The interface employs a drag-and-drop style of interaction and combines a structured natural-language style query specification with reusable multimedia objects. We call this interface DanDMM, short for “drag-and-drop multimedia”. DanDMM interfaces capture the syntax of the underlying query language, and dynamically reconfigure to reflect the contents of the data repository. A distinguishing feature of DanDMM is its ability to synthesize integrated interfaces that incorporate both example-based specification using multimedia objects, and traditional techniques including keyword, attribute, and free text-based search. We describe the DanDMM-builder, a framework for synthesizing DanDMM interfaces, and give several examples of interfaces that have been constructed using DanDMM-builder, including a remote-sensing library application and a video digital library. Received: 15 December 1997 / Revised: June 1999     

Intelligent non-visual navigation of complex HTML structures

This paper provides an overview of a project aimed at using knowledge-based technology to improve accessibility of the Web for visually impaired users. The focus is on the multi-dimensional components of Web pages (tables and frames); our cognitive studies demonstrate that spatial information is essential in comprehending tabular data, and this aspect has been largely overlooked in the existing literature. Our approach addresses these issues by using explicit representations of the navigational semantics of the documents and using a domain-specific language to query the semantic representation and derive navigation strategies. Navigational knowledge is explicitly generated and associated to the tabular and multi-dimensional HTML structures of documents. This semantic representation provides to the blind user an abstract representation of the layout of the document; the user is then allowed to issue commands from the domain-specific language to access and traverse the document according to its abstract layout. Published online: 6 November 2002     

UnQL: a query language and algebra for semistructured data based on structural recursion

Abstract. This paper presents structural recursion as the basis of the syntax and semantics of query languages for semistructured data and XML. We describe a simple and powerful query language based on pattern matching and show that it can be expressed using structural recursion, which is introduced as a top-down, recursive function, similar to the way XSL is defined on XML trees. On cyclic data, structural recursion can be defined in two equivalent ways: as a recursive function which evaluates the data top-down and remembers all its calls to avoid infinite loops, or as a bulk evaluation which processes the entire data in parallel using only traditional relational algebra operators. The latter makes it possible for optimization techniques in relational queries to be applied to structural recursion. We show that the composition of two structural recursion queries can be expressed as a single such query, and this is used as the basis of an optimization method for mediator systems. Several other formal properties are established: structural recursion can be expressed in first-order logic extended with transitive closure; its data complexity is PTIME; and over relational data it is a conservative extension of the relational calculus. The underlying data model is based on value equality, formally defined with bisimulation. Structural recursion is shown to be invariant with respect to value equality. Received: July 9, 1999 / Accepted: December 24, 1999     

A complete temporal relational algebra

Various temporal extensions to the relational model have been proposed. All of these, however, deviate significantly from the original relational model. This paper presents a temporal extension of the relational algebra that is not significantly different from the original relational model, yet is at least as expressive as any of the previous approaches. This algebra employs multidimensional tuple time-stamping to capture the complete temporal behavior of data. The basic relational operations are redefined as consistent extensions of the existing operations in a manner that preserves the basic algebraic equivalences of the snapshot (i.e., conventional static) algebra. A new operation, namely temporal projection, is introduced. The complete update semantics are formally specified and aggregate functions are defined. The algebra is closed, and reduces to the snapshot algebra. It is also shown to be at least as expressive as the calculus-based temporal query language TQuel. In order to assess the algebra, it is evaluated using a set of twenty-six criteria proposed in the literature, and compared to existing temporal relational algebras. The proposed algebra appears to satisfy more criteria than any other existing algebra. Edited by Wesley Chu. Received February 1993 / Accepted April 1995     

Movement Awareness for Ubiquitous Game Control

This paper describes a sensing system for recognising and characterising human movements and its application to ubiquitous gaming. In particular this paper considers the control of computer games through players interacting with the physical environment around them in a natural and appropriate manner. This pushes the interface into the environment, and pulls ubiquitous computing into the game. This is achieved using a sentient computing system. Such a system senses the location, motions, actions and even physiological responses of users. This sensory data can be used to interface and control a game. A good example is 3D first-person games and we demonstrate a system in which actions in the game are mapped to similar actions in the real world. Correspondence to: R. Headon, Laboratory for Communications Engineering, Department of Engineering, University of Cambridge, Trumpington Street, Cambridge CB2 1PZ, UK. Email: rph25@cam.ac.uk     

Effects of Airborne Data Link Communication on Demands, Workload and Situation Awareness

An airborne air-to-ground data link communication interface was evaluated in a multi-sector-planning scenario using an Airbus A 340 full flight simulator. In a close-to-reality experimental setting, eight professional crews performed a flight mission in a mixed voice/data link environment. Experimental factors were the medium (voice vs. data link), workload (low vs. high) and the role in the cockpit (pilot flying vs. pilot non-flying). Data link communication and the usability of the newly developed communication interface were rated positively by the pilots, but there is a clear preference for using a data link only in the phase of cruise. Cognitive demands were determined for selected sections of en-route flight. Demands are affected mainly by increased communication needs. In the pilots’ view, although a data link has no effect on safety or the possibilities of intervention, it causes more problems. The subjective workload, as measured with the NASA Task Load Index, increased moderately under data link conditions. A data link has no general effect on pilots’ situation awareness although flight plan negotiations with a data link cause a distraction of attention from monitoring tasks. The use of a data link has an impact on air-to-ground as well as intra-crew communication. Under data link conditions the pilot non-flying plays a more active role in the cockpit. Before introducing data link communication, several aspects of crew resource management have to be reconsidered. Correspondence and offprint requests to: T. Müller, Technical University of Berlin, Institute of Psychology and Ergonomics, Department of Human–Machine Systems, Jebensstrasse 1, 10623 Berlin, Germany.     

Negotiating Use: Making Sense of Mobile Technology

This paper is based on a study of the ways in which a group negotiated the use of a new mobile technology. The group was made up of ski instructors who, during a one-week ski trip, were equipped with a mobile awareness device called the Hummingbird. The group was studied using ethnomethodologically inspired qualitative methods, with the focus on the group members’ different views of the Hummingbird’s intended use. Negotiations of use occurred using two methods: talk and action. The users negotiated issues such as where and when to use the technology, and whether to consider the Hummingbird a work tool or a gadget for social events. Further, the empirical results clearly show how negotiations of new, mobile technology differ from stationary technology.     

Content-based navigation of music using melodic pitch contours

We describe a system which supports dynamic user interaction with multimedia information using content-based hypermedia navigation techniques, specialising in a technique for navigation of musical content. The model combines the principles of open hypermedia, whereby hypermedia link information is maintained by a link service, with content-based retrieval techniques in which a database is queried based on a feature of the multimedia content; our approach could be described as ‘content-based retrieval of hypermedia links’. The experimental system focuses on temporal media and consists of a set of component-based navigational hypermedia tools. We propose the use of melodic pitch contours in this context and we present techniques for storing and querying contours, together with experimental results. Techniques for integrating the contour database with open hypermedia systems are also discussed.     

Deterministic broadcasting in ad hoc radio networks

We consider the problem of distributed deterministic broadcasting in radio networks of unknown topology and size. The network is synchronous. If a node u can be reached from two nodes which send messages in the same round, none of the messages is received by u. Such messages block each other and node u either hears the noise of interference of messages, enabling it to detect a collision, or does not hear anything at all, depending on the model. We assume that nodes know neither the topology nor the size of the network, nor even their immediate neighborhood. The initial knowledge of every node is limited to its own label. Such networks are called ad hoc multi-hop networks. We study the time of deterministic broadcasting under this scenario. For the model without collision detection, we develop a linear-time broadcasting algorithm for symmetric graphs, which is optimal, and an algorithm for arbitrary n-node graphs, working in time . Next we show that broadcasting with acknowledgement is not possible in this model at all. For the model with collision detection, we develop efficient algorithms for broadcasting and for acknowledged broadcasting in strongly connected graphs. Received: January 2000 / Accepted: June 2001     

A Location Model for Communicating and Processing of Context

Location is one of the most important elements of context in ubiquitous computing. In this paper we describe a location model, a spatial-aware communication model and an implementation of the models that exploit location for processing and communicating context. The location model presented describes a location tree, which contains human-readable semantic and geometric information about an organisation and a structure to describe the current location of an object or a context. The proposed system is dedicated to work not only on more powerful devices like handhelds, but also on small computer systems that are embedded into everyday artefact (making them a digital artefact). Model and design decisions were made on the basis of experiences from three prototype setups with several applications, which we built from 1998 to 2002. While running these prototypes we collected experiences from designers, implementers and users and formulated them as guidelines in this paper. All the prototype applications heavily use location information for providing their functionality. We found that location is not only of use as information for the application but also important for communicating context. In this paper we introduce the concept of spatial-aware communication where data is communicated based on the relative location of digital artefacts rather than on their identity. Correspondence to: Michael Biegl, Telecooperation Office (TecO), University of Karlsruhe, Vincenz-Prieβritz-Str. 1 D-76131 Karlsruhe, Germany. Email: michael@teco.edu     

The optimal location of replicas in a network using a READ-ONE-WRITE-ALL policy

We consider the problem of locating replicas in a network to minimize communications costs. Under the assumption that the read-one-write-all policy is used to ensure data consistency, an optimization problem is formulated in which the cost function estimates the total communications costs. The paper concentrates on the study of the optimal communications cost as a function of the ratio between the frequency of the read and write operations. The problem is reformulated as a zero-one linear programming problem, and its connection to the p-median problem is explained. The general problem is proved to be NP-complete. For path graphs a dynamic programming algorithm for the problem is presented. Received: May 1993 / Accepted: June 2001     

A bin picking system based on depth from defocus

It is generally accepted that to develop versatile bin-picking systems capable of grasping and manipulation operations, accurate 3-D information is required. To accomplish this goal, we have developed a fast and precise range sensor based on active depth from defocus (DFD). This sensor is used in conjunction with a three-component vision system, which is able to recognize and evaluate the attitude of 3-D objects. The first component performs scene segmentation using an edge-based approach. Since edges are used to detect the object boundaries, a key issue consists of improving the quality of edge detection. The second component attempts to recognize the object placed on the top of the object pile using a model-driven approach in which the segmented surfaces are compared with those stored in the model database. Finally, the attitude of the recognized object is evaluated using an eigenimage approach augmented with range data analysis. The full bin-picking system will be outlined, and a number of experimental results will be examined. Received: 2 December 2000 / Accepted: 9 September 2001 Correspondence to: O. Ghita     

The Petri Net Kernel An infrastructure for building Petri net tools

The Petri Net Kernel is an infrastructure for building Petri net tools. It relieves the programmer of a Petri net tool from implementing standard operations on Petri nets and a graphical user interface. In this paper, we discuss the motivation, the concepts, and the implementation of the Petri Net Kernel. Published online: 25 July 2001     

Causality and atomicity in distributed computations

Summary. In a distributed system, high-level actions can be modeled by nonatomic events. This paper proposes causality relations between distributed nonatomic events and provides efficient testing conditions for the relations. The relations provide a fine-grained granularity to specify causality relations between distributed nonatomic events. The set of relations between nonatomic events is complete in first-order predicate logic, using only the causality relation between atomic events. For a pair of distributed nonatomic events X and Y, the evaluation of any of the causality relations requires integer comparisons, where and , respectively, are the number of nodes on which the two nonatomic events X and Y occur. In this paper, we show that this polynomial complexity of evaluation can by simplified to a linear complexity using properties of partial orders. Specifically, we show that most relations can be evaluated in integer comparisons, some in integer comparisons, and the others in integer comparisons. During the derivation of the efficient testing conditions, we also define special system execution prefixes associated with distributed nonatomic events and examine their knowledge-theoretic significance. Received: July 1997 / Accepted: May 1998     

Local model checking and protocol analysis

This paper describes a local model-checking algorithm for the alternation-free fragment of the modal mu-calculus that has been implemented in the Concurrency Factory and discusses its application to the analysis of a real-time communications protocol. The protocol considered is RETHER, a software-based, real-time Ethernet protocol developed at SUNY at Stony Brook. Its purpose is to provide guaranteed bandwidth and deterministic, periodic network access to multimedia applications over commodity Ethernet hardware. Our model-checking results show that (for a particular network configuration) RETHER makes good on its bandwidth guarantees to real-time nodes without exposing non-real-time nodes to the possibility of starvation. Our data also indicate that, in many cases, the state-exploration overhead of the local model checker is significantly smaller than the total amount that would result from a global analysis of the protocol. In the course of specifying and verifying RETHER, we also identified an alternative design of the protocol that warranted further study due to its potentially smaller run-time overhead in servicing requests for data transmission. Again, using local model checking, we showed that this alternative design also possesses the properties of interest. This observation points out one of the often-overlooked benefits of formal verification: by forcing designers to understand their designs rigorously and abstractly, these techniques often enable the designers to uncover interesting design alternatives.