Algebraic properties of stochastic effectivity functions

• The paper defines and investigates stochastic effectivity functions.
• Effectivity functions are related to Markov transition systems.
• Morphisms and congruences are defined and investigated for these functions.
• Logical and behavioral equivalence are defined and related to each other.

Effectivity functions are the basic formalism for investigating the semantics game logic. We discuss algebraic properties of stochastic effectivity functions, in particular the relationship to stochastic relations, morphisms and congruences are defined, and the relationship of abstract logical equivalence and behavioral equivalence is investigated.