The early methods for reasoning about concurrent programs dealt with proving that a program satisfied certain properties--usually invariance properties. But, proving particular properties showed only that the program satisfied those properties. There remained the possibility that the program was incorrect because it failed to satisfy…
From the time I discovered the bakery algorithm (see [12]), I was fascinated by the problem of reasoning about a concurrent program without having to break it into indivisible atomic actions. In [33], I described how to do this for behavioral reasoning. But I realized…
The probability distribution function for topological charge contained in a sphere of finite radius is calculated. We find no need to introduce an arbitrary cutoff on instanton scale sizes as this is controlled by the size of the sphere. Recent Monte Carlo calculations reflect qualitatively…
I showed in [27] that there is no invariant way of defining the global state of a distributed system. Assertional methods, such as [23], reason about the global state. So, I concluded that these methods were not appropriate for reasoning about distributed systems. When I…
Three-dimensional surface point data is often useful for r0b0t control and inspection casks. The design of sensors for collecting this data involves many choices, with selections made on the basis of data rate, accuracy, field of view, safety, size, object properties, and the need for…
The structure of chains in the optimal chain decomposition of a periodic schedule S is investigated. A finite oriented graph termed the Linis Graph (LG) is defined which serves as the key for this investigation. The edges of the LG are trip-types of S and…
In "A new implementation for applicative languages" Turner uses combinators to implement lambda expressions. This paper describes an experimental investigation of the efficiency of Turner's technique compared to more traditional reducers.
We prove a forgetful determinacy theorem saying that, for a wide class of infinitary games, one of the players has a winning strategy that is virtually memoryless: the player has to remember only bounded many bits of information. We use forgetful determinacy to give a…
Answering a question of Jeffrey Ullman, we prove that the problem in the title is shown to be undecidable.
A method of existential interpretation was introduced in [2]. It allows proving undecidability of modest strata of many first order theories. Here we improve the method and its presentation, strengthen somewhat the previous results and prove a couple of new results. The reader is not…
In the case of unbounded buffers, the negative answer follows from a result in [28].
Two small classes of first order formulae without function symbols but with identity, in prenex conjunctive normal form wit hall disjunctions binary, are shown to have a recursively unsolvable decision problem, whereas for another such class an algorithm is developed which solves the decision problem…
