Process Behaviour: Formulae vs. Tests (Extended Abstract)

TL;DR

This paper compares two approaches to defining process behaviour—test satisfaction and logical properties—by characterizing their equivalence through extensional testing and a recursive logic, revealing their precise correspondence.

Contribution

It provides a formal characterization of which logical properties can be captured by tests, establishing the exact correspondence between tests and a subset of process logic.

Findings

Tests and logical properties are equivalent for a specific subset of process properties.

A recursive version of HML captures exactly the properties expressible by tests.

The paper formalizes the relationship between testing and logical characterizations of process behaviour.

Abstract

Process behaviour is often defined either in terms of the tests they satisfy, or in terms of the logical properties they enjoy. Here we compare these two approaches, using extensional testing in the style of DeNicola, Hennessy, and a recursive version of the property logic HML. We first characterise subsets of this property logic which can be captured by tests. Then we show that those subsets of the property logic capture precisely the power of tests.