Jim Morris was a PhD student of Yuri Gurevich at the Electrical Engineering and Computer Science Department of the University of Michigan, the first PhD student working on the abstract state machine project. This is an extended abstract of 1988 Jim Morris's PhD thesis (with…
The chapter consists of two quite different parts. The first part is a survey (including some new results) on finite model theory. One particular point deserves a special attention. In computer science, the standard computation model is the Turing machine whose inputs are strings; other…
Temporal reasoning in complex environments often involves the interpretation of evidence under uncertainty. We have been studying the application of probabilistic reasoning techniques to the problem of temporal-data interpretation. In this report, we discuss techniques for inferring the probability of current hypothesis given temporal evidence.…
Refinement mappings are used to prove that a lower-level specification correctly implements a higher-level one. We consider specifications consisting of a state machine (which may be infinite-state) that specifies safety requirements, and an arbitrary supplementary property that specifies liveness requirements. A refinement mapping from a…
Despite their different perspectives, artificial intelligence (AI) and the disciplines of decision science have common roots and strive for similar goals. This paper surveys the potential for addressing problems in representation, inference, knowledge engineering, and explanation within the decision-theoretic framework. Recent analyses of the restrictions…
One contribution of the article was to formulate Kolmogorov-Uspensky thesis. In "To the Definition of an Algorithm" [Uspekhi Mat. Nauk 13:4 (1958), 3-28 (Russian)] Kolmogorov and Uspensky wrote that they just wanted to comprehend the notions of computable functions and algorithms, and to convince themselves…
The authors introduce a novel pixel-based (iconic) algorithm that estimates depth and depth uncertainty at each pixel and incrementally refines these estimates over time. They describe the algorithm for translations parallel to the image plane and contrast its formulation and performance to that of a…
Intermedia is a hypermedia system developed for use in university research and teaching. It provides a framework for object-oriented, direct-manipulation editors and applications, and the capability to link materials created with those applications. Instructors are able to construct explanatory environments for their students as well…
Let G=(v, E)be a graph and let A and B be sets of vertices. A dominates B if every vertex in B -A is adjacent to at least one vertex in A; A totally dominates B if every vertex in B is adjacent to at…
Dijkstra's EWD 1013, Position Paper on "Fairness", argues that fairness is a meaningless requirement because it can't be verified by observing a system for a finite length of time. The weakness in this argument is revealed by observing that it applies just as well to…
This paper describes an example I came across in which the explicit control predicates introduced in [47] lead to a simpler proof than do dummy variables. This example served as an excuse. The real reason for publishing it was to lobby for the use of…
The Cedar File System (CFS) is a workstation file system that provides access to both a workstation’s local disk and to remote file servers via a single hierarchical name space. CFS supports a group of cooperating programmers by allowing them to both manage local naming…
