Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Logical characterisations, rule formats and compositionality for input-output conformance simulation

Luca Aceto, Ignacio Fábregas, Carlos Gregorio-Rodríguez, Anna Ingólfsdóttir

TL;DR

This work develops a comprehensive theory for input-output conformance simulation, $\mathsf{ioco\underline{s}}$, by providing modal characterisations, a GSOS-based precongruence rule format, and a compositional framework via modal decomposition. It introduces dual modal logics and fixed-point extensions to capture infinite behaviours, and derives characteristic formulae that exactly characterize $\mathsf{ioco\underline{s}}$-relations on finite processes. The paper clarifies the relationship between $\mathsf{ioco\underline{s}}$ and the classical $\mathsf{ioco}$, including counterexamples showing they do not coincide in general, and positions a modular verification pipeline through decomposition and quiescence-aware rule formats. Together, these contributions enable compositional model checking for MBT under a branching-time conformance notion and set the stage for extending the theory to internal actions and hiding.

Abstract

Input-output conformance simulation (iocos) has been proposed by Gregorio-Rodríguez, Llana and Martínez-Torres as a simulation-based behavioural preorder underlying model-based testing. This relation is inspired by Tretmans' classic ioco relation, but has better worst-case complexity than ioco and supports stepwise refinement. The goal of this paper is to develop the theory of iocos by studying logical characterisations of this relation, rule formats for it and its compositionality. More specifically, this article presents characterisations of iocos in terms of modal logics and compares them with an existing logical characterisation for ioco proposed by Beohar and Mousavi. It also offers a characteristic-formula construction for iocos over finite processes in an extension of the proposed modal logics with greatest fixed points. A precongruence rule format for iocos and a rule format ensuring that operations take quiescence properly into account are also given. Both rule formats are based on the GSOS format by Bloom, Istrail and Meyer. The general modal decomposition methodology of Fokkink and van Glabbeek is used to show how to check the satisfaction of properties expressed in the logic for iocos in a compositional way for operations specified by rules in the precongruence rule format for iocos .

Logical characterisations, rule formats and compositionality for input-output conformance simulation

TL;DR

This work develops a comprehensive theory for input-output conformance simulation, , by providing modal characterisations, a GSOS-based precongruence rule format, and a compositional framework via modal decomposition. It introduces dual modal logics and fixed-point extensions to capture infinite behaviours, and derives characteristic formulae that exactly characterize -relations on finite processes. The paper clarifies the relationship between and the classical , including counterexamples showing they do not coincide in general, and positions a modular verification pipeline through decomposition and quiescence-aware rule formats. Together, these contributions enable compositional model checking for MBT under a branching-time conformance notion and set the stage for extending the theory to internal actions and hiding.

Abstract

Input-output conformance simulation (iocos) has been proposed by Gregorio-Rodríguez, Llana and Martínez-Torres as a simulation-based behavioural preorder underlying model-based testing. This relation is inspired by Tretmans' classic ioco relation, but has better worst-case complexity than ioco and supports stepwise refinement. The goal of this paper is to develop the theory of iocos by studying logical characterisations of this relation, rule formats for it and its compositionality. More specifically, this article presents characterisations of iocos in terms of modal logics and compares them with an existing logical characterisation for ioco proposed by Beohar and Mousavi. It also offers a characteristic-formula construction for iocos over finite processes in an extension of the proposed modal logics with greatest fixed points. A precongruence rule format for iocos and a rule format ensuring that operations take quiescence properly into account are also given. Both rule formats are based on the GSOS format by Bloom, Istrail and Meyer. The general modal decomposition methodology of Fokkink and van Glabbeek is used to show how to check the satisfaction of properties expressed in the logic for iocos in a compositional way for operations specified by rules in the precongruence rule format for iocos .
Paper Structure (17 sections, 28 theorems, 37 equations)

This paper contains 17 sections, 28 theorems, 37 equations.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Logic for $\mathbin{\mathsf{ioco\underline{s} }}$
  4. Related logics
  5. Adding fixed points to the logics
  6. Characteristic formulae
  7. The relation between $\mathbin{\mathsf{ioco\underline{s} }}$ and $\mathbin{\mathsf{ioco}}$
  8. The relation with a logic for $\mathbin{\mathsf{ioco}}$
  9. Rule formats for $\mathbin{\mathsf{ioco\underline{s} }}$
  10. Congruence rule format
  11. The rule format cannot be relaxed easily
  12. Applying modal decomposition
  13. A rule format for coherent quiescent behaviour
  14. Conclusion
  15. Proof of Theorem \ref{['thm:congruence']}
  16. ...and 2 more sections

Key Result

Proposition 1

For each logic $\mathcal{L}_{}$, the binary relation $\leq_{\mathcal{L}_{}}$ is a preorder.

Theorems & Definitions (101)

  • Definition 1
  • Definition 2
  • Example 1
  • Remark 1
  • Definition 3
  • Definition 4
  • Proposition 1
  • Definition 5
  • Remark 2
  • Theorem 2
  • ...and 91 more