Have imperative programs been defined like this? Possibly improper definition $\;$ An imperative program is a labeled directed graph, with every vertices labeled by a command and every edge labeled by a predicate.

Denote an edge labeled by predicate $p$ from $x$ to $y$ by $(x, p, y)$,


Two consecutive steps are expressed as $(x, \top, y)$. "Goto" is also expressed in this way.
A binary branch is expressed as $\{(x, p, y), (x, \neg p, z)\}$.


As can be easily noticed, "command" is not defined. I do not know what that should be, but it should be as weak as possible.

Have imperative programs been defined like that?

I also think a mathematical definition could help me go further understanding the space of imperative programs.
Short answer: yes.

Longer answer -- there probably isn't a unique reference but control flow graphs (essentially what you describe) and their precursors, flowcharts are Old. Here are three random references from antiquity to something very recent that use minor modifications of the model. The latter two define the model fairly precisely. You'll find a lot of lattices in the second paper.


Assigning Meaning to Programs, Robert Floyd, 1967.
Systematic Design of Program Transformation Frameworks by Abstract Interpretation, Patrick Cousot and Radhia Cousot, POPL 2002.
Assertion Checking Unified, Sumit Gulwani and Ashish Tiwari, VMCAI 2007.