Source-linked AI summary
Talking quiescence: a rigorous theory that supports parallel composition, action hiding and determinisation
Gerjan Stokkink, Mark Timmer, Mariëlle Stoelinga
TL;DR
Quiescence—the absence of outputs—matters in system modelling, but it remained unclear how common operators could be lifted to quiescence. The paper introduces quiescent transition systems and shows that their restrictions are preserved by common operations.
Problem
Quiescence is important in behavioural modelling, yet it was open whether parallel composition and hiding could be lifted to systems that model it.
Source: §1 · pp. 1–2Method
The paper introduces QTSs, which represent quiescence explicitly with δ-transitions, impose four restrictions, and define common operations directly on QTSs.
Source: §1 · p. 2, §6 · p. 14Results
The four QTS restrictions are preserved by parallel composition, determinisation, and action hiding.
Source: §1 · p. 3, §6 · p. 14Takeaways & Limitations
The framework defines ioco in terms of QTSs, simplifying the theory of model-based testing.
Source: §6 · p. 15The initial theory covers input-enabled, convergent QTSs; relaxing these restrictions is left for future work.
Source: §1 · p. 2
Abstract
from arXiv · showhide
The notion of quiescence - the absence of outputs - is vital in both behavioural modelling and testing theory. Although the need for quiescence was already recognised in the 90s, it has only been treated as a second-class citizen thus far. This paper moves quiescence into the foreground and introduces the notion of quiescent transition systems (QTSs): an extension of regular input-output transition systems (IOTSs) in which quiescence is represented explicitly, via quiescent transitions. Four carefully crafted rules on the use of quiescent transitions ensure that our QTSs naturally capture quiescent behaviour. We present the building blocks for a comprehensive theory on QTSs supporting parallel composition, action hiding and determinisation. In particular, we prove that these operations preserve all the aforementioned rules. Additionally, we provide a way to transform existing IOTSs into QTSs, allowing even IOTSs as input that already contain some quiescent transitions. As an important application, we show how our QTS framework simplifies the fundamental model-based testing theory formalised around ioco.
1 Introduction
Quiescence matters in modelling and testing because an absence of outputs may be correct in one state and erroneous in another. The paper introduces QTSs as a formal framework for representing quiescence and supporting system operations and model-based testing.
1 Introduction
- A quiescent ATM state after dispensing money must not output again until further input, while the state before dispensing should not be quiescent.Quiescence therefore affects whether an observed absence of output is acceptable.Source: §1 · p. 1
- Earlier treatments did not make suspension automata standalone specification entities or define parallel composition and hiding for them.The status of those operators in a quiescence setting was therefore an open question.Source: §1 · p. 2
- QTSs explicitly represent quiescence with δ-transitions as standalone, potentially nondeterministic systems, unlike suspension automata built by adding δ-transitions and determinising.The theory also restricts δ-transition use to rule out counterintuitive behaviour, such as an output following δ or observation of quiescence enabling behaviour.Source: §1 · p. 2
- The paper defines parallel composition, hiding, and determinisation on QTSs, and deltafication can transform IOTSs that already contain δ-transitions.The four QTS requirements are preserved by these operations.Source: §1 · pp. 2–3
- The QTS framework is applied to simplify model-based testing, including defining ioco and aiding test-case generation and evaluation.The paper presents this as an application of its theory.Source: §1 · p. 3
- Detailed proofs of all lemmas, propositions, and theorems are referred to because of space limitations.Source: §1 · p. 3
2 Background
The background establishes the transition-system notation and input/output model used by the paper, then introduces determinisation, parallel composition, hiding, and their trace properties.
2.1 Preliminaries
- The preliminaries define sequences over an action set, prefix and maximality, and the power set notation used in the transition-system definitions.Source: §2.1 · p. 3
2.2 Input-Output Transition Systems
- IOTSs extend labelled transition systems by distinguishing input and output labels and requiring every input to be enabled in every state.The transition labels also include an unobservable internal action, τ.Source: §2.2 · pp. 3–4
2.3 Operations on IOTSs
- Determinisation represents states as nonempty subsets of the original states, with transitions to the states reachable by the action.Source: §2.3 · p. 6
- Parallel composition synchronises on shared inputs and complementary input-output pairs, while hiding renames selected output actions to τ.Hiding is restricted to outputs and must not create τ-loops.Source: §2.3 · pp. 6–7
2.4 Properties of IOTSs
- Hiding corresponds to projecting traces onto the remaining labels; composition projections are included in each component’s traces, and full-alphabet synchronisation yields trace intersection.Source: §2.4 · p. 7
3 Quiescent Transition Systems
Quiescent Transition Systems (QTSs) extend IOTSs with δ-transitions for observing the absence of outputs. Their rules constrain quiescent behavior, while operations and closure results support composition and transformation of QTS models.
3.1 Basic notions and requirements
- QTSs add δ-transitions to IOTSs to represent observations of quiescence, while retaining input-enabledness and defining quiescence by the absence of outputs or internal transitions.A state that can still perform an internal step is not quiescent.Source: §3.1 · pp. 7–8
- R1 requires δ-transitions from quiescent states, and R2 requires their destination to remain quiescent.These rules make quiescence observable and prevent an output or internal step before another input.Source: §3.1 · p. 8
- R3 prevents observing quiescence from enabling new traces, while R4 requires traces to remain unchanged across consecutive δ-transitions.The rules address behavior after one or more quiescence observations.Source: §3.1 · p. 9
3.2 Operations on QTSs
- QTS operations include determinisation, parallel composition, and action hiding; parallel composition synchronises components on δ, while hiding converts selected outputs to internal actions.The δ-label cannot be hidden, and hiding must not create divergence.Source: §3.2 · p. 10
3.3 Properties of QTSs
- QTSs are closed under determinisation, action hiding, and parallel composition, and parallel-composition traces obey projection and intersection properties.When components have the same alphabet, the composition’s traces equal the intersection of their individual trace sets.Source: §3.3 · p. 11
4 From IOTS to QTS: deltafication
Deltafication converts an IOTS into a QTS by adding δ-loops to quiescent states that lack them, subject to condition C1 and rules R2–R4. The section establishes when this conversion is valid and how it interacts with hiding, parallel composition, and determinisation.
4 From IOTS to QTS: deltafication
- C1 requires traces from a δ-successor that can reach non-δ quiescence to reach such a state from the source as well.The conversion adds δ-loops only to quiescent states without an existing δ-transition; an existential relaxation of C1 would not suffice.Source: §4 · p. 11
4.1 Validity of deltafication
- Under C1 and R2–R4, deltafication yields a QTS and is idempotent; it also maps δ-free IOTSs and existing QTSs to QTSs.Source: §4.1 · p. 12
4.2 Commutativity results
- Deltafication and determinisation do not necessarily commute; for a nondeterministic IOTS, deltaficate first and then determinise to preserve observable quiescence.The reverse order can lose the observation that quiescence may follow an initial input.Source: §4.2 · pp. 12–13
- Deltafication commutes with hiding and parallel composition, so either operation may be applied before or after conversion without changing the resulting QTS.The paper attributes this flexibility to the way these operations interact with deltafication.Source: §4.2 · p. 13
5 Application to testing
The paper formulates ioco using QTSs, where explicit δ-transitions represent expected absence of outputs. It shows how QTS traces support conformance checking and a straightforward testing procedure.
5.1 A conformance relation based on QTSs
- Explicit δ-transitions represent expected silence, so an implementation’s unexpected absence of output can count as nonconformance.The specification may allow quiescence alongside output actions; the example marks unexpected quiescence with a δ-transition.Source: §5.1 · pp. 13–14
- With input-enabled QTSs, ioco-conformance corresponds precisely to traditional trace inclusion over QTSs.Source: §5.1 · p. 14
- The example distinguishes two ioco-correct implementations from two erroneous ones, including one that is unexpectedly quiescent after c?.The correct implementations may omit specification traces, provided they do not produce an unexpected output after a specification trace.Source: §5.1 · p. 14, Figure 10 · p. 14
5.2 Testing using QTSs
- A test can provide inputs, observe behavior, or stop; the resulting trace, including δ-actions, must also be a specification trace.The paper states that this straightforward procedure precisely corresponds to checking ioco-conformance.Source: §5.2 · p. 14
6 Conclusions and Future Work
The paper concludes that QTSs explicitly model quiescence and provide a basis for operations, IOTS conversion, and ioco testing. Its current framework is limited to input-enabled, convergent systems.
6 Conclusions and Future Work
- QTSs model absence of outputs explicitly, define standard operations directly, and preserve the four QTS restrictions under those operations.Source: §6 · p. 14
- The framework also allows conversion from IOTSs that already partially model quiescence and defines ioco in terms of QTSs.Source: §6 · pp. 14–15
- The current framework covers only input-enabled, convergent QTSs; divergent and not-necessarily-input-enabled systems remain future work.The paper also identifies connecting QTSs to timed automata as future work.Source: §6 · p. 15