A Relational Modal Logic for Higher-Order Stateful Adts