Alternating Simulation and IOCO

8 years 3 months ago
Alternating Simulation and IOCO
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/orefinement 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/orefinement or bounded non-ioco to checking first-order assertions.
Margus Veanes, Nikolaj Bjørner
Added 30 Jan 2011
Updated 30 Jan 2011
Type Journal
Year 2010
Where PTS
Authors Margus Veanes, Nikolaj Bjørner
Comments (0)