  Input-output conformance simulation (iocos) has been proposed by
Gregorio-Rodr\'iguez, Llana and Mart\'inez-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 .
