Linear Constraints as a Modeling Language for Discrete Time Hybrid Systems

Model Based Design is particularly appealing in embedded software design where system level specifications are much easier to define than the control software behavior itself. Formal analysis of Embedded Systems requires modelling both continuous systems (typically, the plant) as well as discrete systems (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 System, where plant dynamics is modeled as a linear predicate over state, input, and next state variables. MILP solvers requires constraints represented as conjunctive predicates. 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 transformed into an equisatisfiable conjunctive predicate. Moreover, since variable bounds play a key role in this transformation, we present an algorithm that taking as input a linear predicate, computes implicit variable bounds.