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.
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.
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.
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.
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