Automating Verification of Cooperation, Control, and Design in Traffic Applications - Formal Methods and Hybrid Real-Time Systems - page 154

7.1 Model Checking Hybrid Systems with Large Discrete State

Spaces

We have proposed an approach for verification of hybrid systems, which con-
tain large discrete state spaces and simple continuous dynamics given as con-
stants [11] (methods dealing with richer dynamics, e.g., given as differential
inclusions, are currently under development). Large discrete state space arise
naturally in industrial hybrid systems, due to the need to represent discrete in-
puts, counters, sanity-check bits, possibly multiple concurrent state machines
etc , which typically jointly with properties of sensor values determine the selec-
tion of relevant control laws. Thus this non-trivial discrete behavior cannot be
treated by considering discrete states one by one as in tools based on the notion
of hybrid automata. We have developed a model checker dealing with ACTL
properties for this application class.

continuous domain variables

...

c 1 c m

boolean domain variables

... d 1 d p FO conditions

mapping between
first-order conditions
and bool. variables

... q 1 q j

AIG

...

φ 1 φ k

Represented first-order
predicates

Fig. 17. The Lin-AIG structure

Representation of state-sets. In our setting, the state-sets of hybrid systems
consist of both discrete states, represented by Boolean formulas, and continuous
regions, represented by a Boolean combination of linear constraints. We use an
extension of And-Inverter-Graphs [39] with linear constraints (Lin-AIGs) as a
compact representation format (see Fig. 17). In Lin-AIGs Boolean formulas are
represented by Functionally Reduced And-Inverter Graphs (FRAIGs), which are
basically Boolean circuits consisting only of AND gates and inverters. In contrast
to BDDs, FRAIGs are not a canonical representation for Boolean functions, but
they are “semi-canonical” in the sense that every node in the FRAIG represents
a unique Boolean function. To be able to use FRAIGs to represent continuous
regions, we introduce a set of new (Boolean) constraint variables Q as encodings
for linear constraints, where each occurring linear constraint is represented by
some q Q as illustrated in Fig. 17. Thus we arrive at state-sets encoded by

Boolean formulas over Boolean variables and Q , together with a mapping of Q
into linear constraints.

∈