Multirelations with infinite computations

• We describe operations and properties of multirelations in terms of relations.
• We extend multirelations to represent finite and infinite computations independently.
• We characterise multirelations that model strict computations.
• We use RelView to derive an approximation order for multirelations.
• The approximation order uses only weak assumptions in pointed distributive lattices.

Multirelations model computations with both angelic and demonic non-determinism. We extend multirelations to represent finite and infinite computations independently. We derive an approximation order for multirelations assuming only that the endless loop is its least element and that the lattice operations are isotone. We use relations, relation algebra and RelView for representing and calculating with multirelations and for finding the approximation order.