The paper Logical characterisations, rule formats and compositionality for input-output conformance simulation by Luca Aceto, Ignacio Fabregas, Carlos Gregorio-Rodriguez and Anna Ingolfsdottir has been accepted for publication in the Journal of Logical and Algebraic Methods in Programming. The paper is an extended version of a conference paper that appeared in SOFSEM 2017. (See here for a longer author version of the conference paper.)
Input-output conformance simulation (iocos, for short) 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, which is PSPACE-complete, and supports stepwise refinement. The goal of the above-mentioned ICE-TCS paper is to develop the theory of iocos further by studying logical characterisations of that relation, rule formats for it and its compositionality. More specifically, that article presents Hennessy-Milner-like characterisations of iocos in terms of modal logics and compares them with an existing logical characterisation for ioco proposed by Beohar and Mousavi. The article also offers a characteristic-formula construction for iocos over finite processes in an extension of the proposed modal logics with greatest fixed points, and provides 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.
In a forthcoming post, I will describe the notion of characteristic formula and some of the results in a recent ICE-TCS preprint that studies the complexity of determining whether a formula expressed in a modal logic, possibly with fixed points, is characteristic for some finite LTS/Kripke structure.