@techreport{veanes2010alternating,
author = {Veanes, Margus and Bjørner, Nikolaj},
title = {Alternating Simulation and IOCO},
year = {2010},
month = {April},
abstract = {We propose a symbolic framework called guarded labeled assignment systems or GLASs and show how GLASs can be used as a foundation for symbolic analysis of various aspects of formal specification languages. We define a notion of i/o-refinement over GLASs as an alternating simulation relation and provide formal proofs that relate i/o-refinement to ioco. We show that non-i/o-refinement reduces to a reachability problem and provide a translation from bounded non-i/o-refinement or bounded non-ioco to checking first-order assertions.},
publisher = {Microsoft Research},
url = {http://approjects.co.za/?big=en-us/research/publication/alternating-simulation-and-ioco/},
number = {MSR-TR-2010-38},
note = {Extended version of paper with the same title in ICTSS 2010, LNCS vol 6435},
}