Quantitative testing semantics for non-interleaving

TL;DR

This paper introduces a non-interleaving denotational semantics for the ?-calculus, using a semiring-based test outcome framework that generalizes standard may- and must-testing, capturing richer process behaviors.

Contribution

It develops a novel quantitative testing semantics for the ?-calculus based on semirings and modules, extending trace semantics with readiness information.

Findings

Defines a semiring-based test outcome structure.

Generalizes may- and must-testing within the new framework.

Provides a trace semantics with partial orders and readiness.

Abstract

This paper presents a non-interleaving denotational semantics for the ?-calculus. The basic idea is to define a notion of test where the outcome is not only whether a given process passes a given test, but also in how many different ways it can pass it. More abstractly, the set of possible outcomes for tests forms a semiring, and the set of process interpretations appears as a module over this semiring, in which basic syntactic constructs are affine operators. This notion of test leads to a trace semantics in which traces are partial orders, in the style of Mazurkiewicz traces, extended with readiness information. Our construction has standard may- and must-testing as special cases.