University of Leicester

computerscience

Finite Axiom Systems for Testing Preorder and De Simone Process Languages,
Irek Ulidowski,
Theoretical Computer Science, 239, pages 97-139. 2000.

Abstract

We prove that testing preorder of De Nicola and Hennessy is preserved by all De Simone process operators. Based on this result we propose an algorithm for generating axiomatisations of testing preorder for arbitrary De Simone process languages. The axiom systems produced by our algorithm are finite and complete for processes with finite behaviour. In order to achieve completeness for a subclass of processes with infinite behaviour we use one infinitary induction rule.

The usefulness of our results is illustrated in specification and verification of small concurrent systems, where suspension, resumption and alternation of execution of component systems occur. We argue that better specifications can be more easily written in custom-made De Simone process languages which contain both the standard operators as well as new, specially tailored for the task in hand De Simone operators. Moreover, the automatically generated axiom systems for such specification languages make the verification straightforward.

This paper is available in dvi.gz and ps.gz form. If you email me , I can also send you a TCS preprint of this paper.

| [University Home]|[Faculty of Science]|[MCS Home]|[CS Home]||[University Index A-Z]|[University Search]|[University Help]|

Author: Irek Ulidowski (I.Ulidowski@mcs.le.ac.uk).
University of Leicester. Last modified: 12th January 2004, 18:27:04
CS Web Maintainer.