Quantitative Relations and Approximate Process Equivalences

   page       BibTeX_logo.png   
Alessandra Di Pierro, Chris Hankin, Herbert Wiklicky
Roberto M. Amadio, Denis Lugiez (eds.)
CONCUR 2003, pages 498-512
Lecture Notes in Computer Science 2761

We introduce a characterisation of probabilistic transition systems (PTS) in terms of linear operators on some suitably defined vector space representing the set of states. Various notions of process equivalences can then be re-formulated as abstract linear operators re- lated to the concrete PTS semantics via a probabilistic abstract inter- pretation. These process equivalences can be turned into corresponding approximate notions by identifying processes whose abstract operators “differ” by a given quantity, which can be calculated as the norm of the difference operator. We argue that this number can be given a statistical interpretation in terms of the tests needed to distinguish two behaviours.