**Abstract:** Model based design is particularly appealing in

software based control systems (e.g., embedded

software) design, since in such a case system

level specifications are much easier to define

than the control software behavior itself. In

turn, model based design of embedded systems

requires modeling both continuous subsystems

(typically, the plant) as well as discrete

subsystems (the controller). This is typically

done using hybrid systems. Mixed Integer Linear

Programming (MILP) based abstraction techniques

have been successfully applied to automatically

synthesize correct-by-construction control

software for discrete time linear hybrid systems,

where plant dynamics is modeled as a linear

predicate over state, input, and next state

variables. Unfortunately, MILP solvers require

such linear predicates to be conjunctions of

linear constraints, which is not a natural way of

modeling hybrid systems. In this paper we show

that, under the hypothesis that each variable

ranges over a bounded interval, any linear

predicate built upon conjunction and disjunction

of linear constraints can be automatically

translated into an equivalent conjunctive

predicate. Since variable bounds play a key role

in this translation, our algorithm includes a

procedure to compute all implicit variable bounds

of the given linear predicate. Furthermore, we

show that a particular form of linear predicates,

namely guarded predicates, are a natural and

powerful language to succinctly model discrete

time linear hybrid systems dynamics. Finally, we

experimentally show the feasibility of our

approach on an important and challenging case

study taken from the literature, namely the

multi-input Buck DC-DC Converter. As an example,

the guarded predicate that models (with 57

constraints) a 6-inputs Buck DC-DC Converter is

translated in a conjunctive predicate (with 102

linear constraints) in about 40 minutes.

**Keywords:** Model-based software design; Linear predicates; Hybrid systems