Publications (co-) authored by Rance Cleaveland: 1990


Tableau-based model checking in the propositional mu-calculus.
Acta Informatica, 27(8):725--747, September 1990.
Abstract:

This paper describes a procedure, based around the construction of tableau proofs, for determining whether finite-state systems enjoy properties formulated in the propositional mu-calculus. It presents a tableau-based proof system for the logic and proves it sound and complete, and it discusses techniques for the efficient construction of proofs that states enjoy properties expressed in the logic. The approach is the basis of an ongoing implementation of a model checker in the Concurrency Workbench, an automated tool for the analysis of concurrent systems.


On automatically distinguishing inequivalent processes.
In E.M. Clarke and R.P. Kurshan, editors, Computer-Aided Verification '90, volume 3 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 463--477, Piscataway, NJ, June 1990. American Mathematical Society.
Note: The next paper is a corrected version of this one.
On automatically explaining bisimulation inequivalence.
In E.M. Clarke and R.P. Kurshan, editors, Computer-Aided Verification (CAV '90), volume 531 of Lecture Notes in Computer Science, pages 364--372, Piscataway, NJ, June 1990. Springer-Verlag.
Abstract:

This paper describes a technique for generating a logical formula that differentiates between two bisimulation-inequivalent finite-state systems. The method works in conjunction with a partition-refinement algorithm for computing bisimulation equivalence and yields formulas that are often minimal in a precisely defined sense.


Priorities in process algebra.
Information and Computation, 87(1/2):58--77, July/August 1990.
Abstract:

An operational semantics for an algebraic theory of concurrency is developed that incorporates a notion of priority into the definition of the execution of actions. An equivalence based on strong observational equivalence is defined and shown to be a congruence, and a complete axiomatization is given for finite terms. Several examples highlight the novelty and usefulness of our approach.


A preorder for partial process specifications.
In J. Baeten and J. Klop, editors, CONCUR '90, volume 458 of Lecture Notes in Computer Science, pages 141--151. Amsterdam, August 1990. Springer-Verlag.
Abstract:

This paper presents a behavioral preorder for relating partial process specifications to implementations and establishes that it is "adequate" in the following sense: one} specification may be used to characterize all implementations of a network component that are correct for any network context exhibiting a particular interface. This property makes the preorder particularly suitable for reasoning compositionally about networks of processes. The paper also gives a sound and complete axiomatization for finite processes of the largest precongruence contained in this new preorder.


When is "partial" adequate? A logic-based proof technique using partial specifications.
In Fifth Annual Symposium on Logic in Computer Science (LICS '90), pages 440--449, Philadelphia, June 1990. IEEE Computer Society Press.
Abstract:

This paper presents a technique for ascertaining when a (finite-state) partial process specification is adequate, in the sense of being "specified enough," for contexts in which it is to be used. The method relies on the automatic generation of a modal formula from the partial specification; if the remainder of the network satisfies this formula then any process that meets the specification is guaranteed to ensure correct behavior of the overall system. Using our results, we develop compositional proof rules for establishing the correctness of networks of parallel processes, and we illustrate their use with several examples.


Go to Rance Cleaveland's publication home page.

Last modified: August 13, 1998

Rance Cleaveland
rance@cs.sunysb.edu