A Linear-Time Branching-Time Spectrum for Behavioral Specification Theories

TL;DR

This paper develops a unified framework for behavioral specification theories across most equivalences in the linear-time--branching-time spectrum, extending beyond bisimilarity to other preorders and equivalences.

Contribution

It introduces a general scheme for defining behavioral specification theories using disjunctive modal transition systems for a wide range of equivalences.

Findings

Specification theories for preorders cannot exist.

A general scheme for behavioral specification theories is proposed.

Applicable to most equivalences in the spectrum.

Abstract

We propose behavioral specification theories for most equivalences in the linear-time--branching-time spectrum. Almost all previous work on specification theories focuses on bisimilarity, but there is a clear interest in specification theories for other preorders and equivalences. We show that specification theories for preorders cannot exist and develop a general scheme which allows us to define behavioral specification theories, based on disjunctive modal transition systems, for most equivalences in the linear-time--branching-time spectrum.