Publications (co-) authored by Rance Cleaveland: 1995


Efficient on-the-fly model checking for CTL*.
In Tenth Annual Symposium on Logic in Computer Science (LICS '95), pages 388--397, San Diego, June 1995. IEEE Computer Society Press.
Abstract:

This paper gives an on-the-fly algorithm for determining whether a finite-state system satisfies a formula in the temporal logic CTL*. The time complexity of our algorithm matches that of the best existing ``global algorithm'' for model checking in this logic, and it performs as well as the best known global algorithms for the sublogics CTL and LTL. In contrast with these approaches, however, our routine constructs the state space of the system under consideration in a need-driven fashion and will therefore perform better in practice.


E. Brinksma, R. Cleaveland, K.G. Larsen, and B. Steffen, editors.
Tools and Algorithms for the Construction and Analysis of Systems (TACAS '95), volume 1019 of Lecture Notes in Computer Science, Aarhus, Denmark, May 1995. Springer-Verlag.

Generating diagnostic information for behavioral preorders.
Distributed Computing, 9:61--75, 1995.
Abstract:

This paper describes a method for generating diagnostic information that explains why a given finite-state system fails to be greater than its specification with respect to the prebisimulation preorder. The information takes the form of a logical formula satisfied by the specification but not by the system and thus may be used by system designers for debugging purposes. Our technique relies on modifying an algorithm for computing the prebisimulation preorder so that information needed for generating these distinguishing formulas is saved appropriately. As a number of other behavioral preorders may be characterized in terms of prebisimulation preorder, our approach may be used as a basis for computing diagnostic information for these relations as well.


Optimality and abstraction in model checking.
In A. Mycroft, editor, Static Analysis, volume 983 of Lecture Notes in Computer Science, pages 51--63, Glasgow, UK, September 1995. Springer-Verlag.
Abstract:

This paper investigates the use of abstract-interpretation-inspired techniques for improving the performance of procedures for determining when systems satisfy formulas in branching-time temporal logic. A framework for abstracting system descriptions is developed, and a particular method for generating abstract systems from given abstractions on system states is defined and shown to be both safe and optimal, in the sense that concrete systems satisfy all the temporal formulas enjoyed by their abstracted counterparts. One may then use a model checker on an abstracted (and hence smaller) system in order to infer properties of a concrete system.


Generating front ends for verification tools.
In E. Brinksma, R. Cleaveland, K.G. Larsen, and B. Steffen, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS '95), volume 1019 of Lecture Notes in Computer Science, Aarhus, Denmark, May 1995. Springer-Verlag.
Abstract:

This paper describes the Process Algebra Compiler (PAC), a front-end generator for process-algebra-based verification tools. Given descriptions of a process algebra's concrete and abstract syntax and semantics as structural operational rules, the PAC produces syntactic routines and functions for computing the semantics of programs in the algebra. Using this tool greatly simplifies the task of adapting verification tools to the analysis of systems described in different languages; it may therefore be used to achieve source-level compatibility between different verification tools. Although the initial verification tools targeted by the PAC are MAUTO and the Concurrency Workbench, the structure of the PAC caters for the support of other tools as well.


Divergence and Fair Testing.
In Zoltan Fulop and Ferenc Gecseg, editors, Automata, Languages and Programming (ICALP '95), volume 944 of Lecture Notes in Computer Science, pages 648--659, Szeged, Hungary, July 1995. Springer-Verlag.
Abstract:

This paper develops a new testing-based semantic theory of processes that aims to circumvent difficulties that traditional testing/failures theories have in dealing with divergent behavior. Our framework incorporates a notion of fairness into the determination of when a process passes a test; we contrast this definition with existing approaches and give characterizations of the induced semantic preorders. An example highlights the utility of our results.


Go to Rance Cleaveland's publication home page.

Last modified: August 13, 1998

Rance Cleaveland
rance@cs.sunysb.edu