Publications (co-) authored by Rance Cleaveland: 1992

Computing diagnostic tests for incorrect processes.

In Proceedings of the IFIP Symposium on Protocol Specification, Testing and Verification, pages 263--278, Lake Buena Vista, Floriday, June 1992. North-Holland.

This paper presents a method for generating diagnostic tests that is to be used in conjunction with an algorithm for computing the testing preorder of Hennessy and DeNicola. These tests may be used to debug a finite-state system that fails to meet (i.e be larger in the testing preorder than) a specification; in this case, the system is guaranteed to fail the test that is produced, while the specification is guaranteed to pass it. Our technique relies on transforming the diagnostic information produced by a general preorder algorithm into tests when the general preorder algorithm is used to compute the testing preorder. The method does not affect the time complexity of computing the relation.

On computing diagnoatic information for preorder checking.

In G.v. Bochmann and D. Probst, editors, Computer-Aided Verification (CAV '92), volume 663 of Lecture Notes in Computer Science, pages 370--383, Montreal, June/July 1992. Springer-Verlag.

This paper describes a method for generating diagnostic information for the prebisimulation preorder. This information takes the form of a logical formula explaining why a particular process is not larger than the other in the preorder. Our method relies on modifying an algorithm for computing the prebisimulation preorder to save the information needed for generating these distinguishing formulas. As a number of other behavioral preorders may be characterized in terms of prebisimulation preorder, our technique may be used as a basis for computing diagnostic information for these preorders as well.

Note: A journal version subsumes this paper.

R. Cleaveland, editor.

CONCUR '92, volume 630 of Lecture Notes in Computer Science. Springer-Verlag, Stony Brook, New York, August 1992.

Faster model checking for the modal mu-calculus.

In G.v. Bochmann and D. Probst, editors, Computer-Aided Verification (CAV '92), volume 663 of Lecture Notes in Computer Science, pages 410--422, Montreal, June/July 1992. Springer-Verlag.

In this paper, we develop an algorithm for model checking that handles the full modal mu-calculus including alternating fixpoints. Our algorithm has a better worst-case complexity than the best known algorithm for this logic while performing just as well on certain sublogics as other specialized algorithms. Important for the efficiency is an alternative characterization of formulas in terms of equational systems, which enables the sharing and reuse of intermediate results.

Note: The version of this paper that is available is greatly expanded from what appears in the proceedings.

Testing preorders for probabilistic processes.

In W. Kuich, editor, Automata, Languages and Programming (ICALP '92), volume 623 of Lecture Notes in Computer Science, pages 708--719, Vienna, July 1992. Springer-Verlag.

We present a testing preorder for probabilistic processes based on the natural notion of a process passing a test with a certain probability. The theory enjoys close connections with the classical testing theory of Hennessy and DeNicola in that whenever a process passes a test with probability 1 (respectively some non-0 probability) in our setting, then the process must (respectively may) pass the test in the classical theory. In addition, we develop an alternative characterization of the probabilistic testing preorder that is based on the "must sets" characterization of De Nicola. Finally, we extend our theory of testing to substochastic processes, in which the sum of the probabilities of a process's outgoing transitions may be strictly less than 1, with the deficit representing the process' capacity for undefined behavior. A simple example involving the construction of pipelines from faulty buffer cells is given to illustrate how substochastic processes, and the resulting preorder, can be used to model fault-tolerant systems and to reason about system reliability.

M. Stallmann, R. Cleaveland, and P. Hebbar.

GDR: A Visualization Tool for Graph Algorithms.

In N. Dean and G. Shannon, editors, Computational Support for Discrete Mathematics, volume 15 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 17--28, Piscataway, NJ, March 1992. American Mathematical Society. (Proceedings published in early 1994.)

This paper describes GDR, a tool for editing graphs and animating graph algorithms. The design of GDR emphasizes simplicity and the ability to interact with other tools. GDR has been used to implement classroom animations of graph algorithms and finite automata, and as a research tool for prototyping algorithms.

Note: Interested parties should contact Matt Stallmann for a copy of this paper.

Last modified: August 13, 1998