Animal brain is able to replace the function of one sensory modality into another, which is known as sensory substitution. This cross-modal plasticity has mainly been studied to replace the lost of certain animal sensation, such as visual or auditory perception. The most studied fields are Braille reading and visual information transportation for blind people. Recent studies have developed non-invasive simulation systems using audio or electrotactile signals for visual substitution.

However, how to theoretically assure that one sensory modality can simulate the other is a fundamental question and has been rarely studied in literatures. With experiments and real-life data, this work aims to establish formal syntax and semantics for sensory modality to capture the behaviours of tactile/audition and visual sensations. Based on pi-calculus, a famous behavioural theory in computer science, we prove that targeted modality models are bisimilar or even equivalent. As a contribution, our theory provides the key basis for reasoning and constructing sensory substitution.