Quotient of Acceptance Specifications under Reachability Constraints

TL;DR

This paper introduces a quotient operation for marked acceptance specifications (MAS) that guarantees reachability constraints, facilitating incremental design and synthesis of specifications in automata-based models.

Contribution

It defines a sound and complete quotient operation for MAS, ensuring reachability properties and advancing specification theory for automata with variability.

Findings

A new quotient operation for MAS is proposed.

The quotient guarantees reachability constraints by construction.

The operation is proven to be sound and complete.

Abstract

The quotient operation, which is dual to the composition, is crucial in specification theories as it allows the synthesis of missing specifications and thus enables incremental design. In this paper, we consider a specification theory based on marked acceptance specifications (MAS) which are automata enriched with variability information encoded by acceptance sets and with reachability constraints on states. We define a sound and complete quotient for MAS hence ensuring reachability properties by construction.