Have action/predicate systems (or similar) been considered in the literature? Question. Has the following concept, or anything similar, been considered in the literature?
Definition. An action/predicate system consists of sets $A$ (the actions) and $X$ (the predicates) such that the following hold.


*

*$A$ forms a monoid

*$X$ forms a Boolean lattice

*There is a monoid action $A \times X \rightarrow X$ denoted $ax$, such that for all $a \in A$ we have that the function $x \in X \mapsto ax \in X$ is an endomorphism of $X$. Intuitively, $ax$ means "the predicate that returns $\mathtt{True}$ in precisely those states where $a$ brings about $x$."

*There is a function $\sim \,: A \times A \rightarrow X$ subject to the following axioms. Intuitively, $a \sim b$ means "the predicate that returns $\mathtt{True}$ in precisely those states where $a$ has the same effect as $b$." 


*

*Reflexivity.   $\forall a \in A : \top \leq (a \sim a)$

*Symmetry.      $\forall a,b \in A : (a \sim b) \leq (b \sim a)$

*Transitivity.  $\forall a,b,c \in A : (a \sim b) \wedge (b \sim c) \leq (a \sim c)$

*Compatibility I. $$\forall a,b,c \in A : (a \sim b) \leq (ac \sim bc),\quad \forall a,b,c \in A : (a \sim b) \leq (ca \sim cb)$$

*Compatibility II. $\forall a,b \in A,\;\forall x \in X : (a \sim b) \leq (ax \leftrightarrow bx)$



Reiteration of Question. Has this been considered in the literature? And if so, what is the correct terminology for such structures, and where can I learn more?
Intuition. Firstly, we can think of actions as being "commands" in a programming language; they move the machine to a new state, depending on its current state. The unit $1 \in A$ is the command that does nothing; furthermore, if $a$ and $b$ are commands, then $ab$ is the result of first performing $a$, then $b$.
Secondly, we can think of predicates as being... well, predicates; in the sense of returning true/false depending on the current state of the machine. Furthermore, if $a$ is an action and $x$ is a predicate, then $ax$ can be thought of as the predicate that returns $\mathtt{true}$ for precisely those states in which the action $a$, if performed, would bring about $x$. Thus we may read "$ax"$ as "$a$ brings about $x$."
Thirdly, the stipulation that the aforementioned action be a homomorphism of boolean algebras can be motivated by the observation that the following statements ought to be equivalent.


*

*We're in a state such that performing $a$ would bring about $x \vee y$.

*We're in a state such that either performing $a$ would bring about $x$, or performing $a$ would bring about $y$.


This corresponds to the axiom $a(x \vee y) = ax \vee ay$. Similar linguistic reasoning can motivate the remainder of the homomorphism stipulation.
Fourthly and finally, the function $\sim : A \times A \rightarrow X$ can be given the following interpretation. If $a,b \in A$ are actions, then $a \sim b$ is the predicate that returns $\mathtt{true}$ for precisely those states in which enacting $a$ would change the machine to the same state as would enacting $b$. The axioms associated with $\sim$ are motivated on this basis.
A bit more motivation. Here's some basic stuff that we can express in this language.


*

*In any state where $x$ holds, we have that $a$ brings about $y$.


$$x \leq ay$$


*

*In general, the action $a$ brings about that $x$ implies $y$.


$$\top \leq a(x \rightarrow y)$$


*

*In any state where $x$ holds, $a$ has the same effect as $b$.


$$x \leq (a \sim b)$$
 A: The first three conditions indeed correspond to the action of a monoid on a Boolean algebra, but the fourth condition is of a different nature. Let me introduce another function $d: A \times A \to X$ by setting $d(a, b) = (a \sim b)'$. Rewriting the four axioms gives


*

*For all $a \in A$, $d(a,a) = 0$ ($0$ stands for $\bot$, but seems more appropriate in this context).

*For all $a,b \in A$, $d(a,b) = d(b,a)$.

*For all $a,b, c \in A$, $d(a,c) \leqslant d(a,b) \vee d(b,c)$

*For all $a,b \in A$, and $x \in X$, $ax\ \Delta\ bx \leqslant d(a,b)$ where $x\ \Delta\ y$ is the symmetric difference of $x$ and $y$.


Now, the first three axioms are reminiscent of the definition of a Boolean metric. The missing bit is $d(a, b) = 0$ implies $a = b$, but we are very close to it. Indeed if $d(a, b) = 0$, then by (4) $ax\ \Delta\ bx = 0$, whence $ax = bx$ for all $x$.
The notion of a Boolean metric space dates back at least from the fifties. You can easily find references on the web. I found this early one, but unfortunately I do not have access to this paper.
Blumenthal, L. M. Boolean Geometry I. Rend. Circ. Mat. Palermo. 1952, 1, 343-360.
A: Disclaimer: I am no expert, but here are my thoughts.
With your algebraic definitions, you have essentially described the mu-calculus used in program model checking. Mu calculus is defined in terms of actions and lattices just as in your description. 
In addition, the equivalence relation you have defined seems analogous to the concept of predicate abstraction. Predicate abstraction is used to reduce the state space of a program by identifying actions that are equivalent modulo some predicate.
You might check the following to see if this is the case:
http://en.wikipedia.org/wiki/Modal_%CE%BC-calculus
http://www.cs.ucla.edu/~todd/research/pldi01.pdf
