CHAPTER 4. SIMPLIFICATIONS
CHAPTER 4. SIMPLIFICATIONS
Table 4.5: Inequality Simplifications Xm
i=1
aixi+at[true]≥n→ Xm i=1
aixi≥n−at (4.29)
Xm i=1
aixi+at¬[true]≥n→ Xm i=1
aixi≥n (4.30)
Xm i=1
aixi+aj1xj+aj2xj ≥n→ Xm i=1
aixi+ (aj1+aj2)xj ≥n (4.31) Xm
i=1
aixi+ajxj+aj¬xj ≥n→ Xm i=1
aixi ≥n−aj (4.32)
aj1> aj2
Xm i=1
aixi+aj1xj+aj2¬xj≥n→ Xm i=1
aixi+ (aj1−aj2)xj≥n−aj2
(4.33)
aj1< aj2
Xm i=1
aixi+aj1xj+aj2¬xj≥n→ Xm i=1
aixi+ (aj2−aj1)¬xj ≥n−aj1
(4.34)
The reader should keep the commutativity and associativity of the + operator in mind when viewing the rules; these are not the complete set.
Table 4.6: Clause Simplifications _m
i=1
xi∨[true]→[true] (4.35)
_m i=1
xi∨ ¬[true]→ _m i=1
xi (4.36)
_m i=1
xi∨xj∨xj → _m i=1
xi∨xj (4.37)
_m i=1
xi∨xj∨ ¬xj→[true] (4.38)
The reader should keep the commutativity and associativity of the ∨operator in mind when viewing the rules; these are not the complete set.
Chapter 5
DC Formulas with Models of Elementary Length
Generally, the shortest models of DC formulas may have non-elementary length, as shown in [MF02]. One may therefore wonder if it really makes sense to use bounded model checking for validating DC formulas; it may be of questionable value to know that a particular formula has no models of some lengthkif this provides no guarantee that it may not have models of length> k.
However, for a class of DC formulas, we can achieve the desired property of a bound on the model length, as these formulas have models of elementary length, if any. In [MF02] it is argued that this is the case for any formula that does not contain unguarded negations. A guarded formula ψ occurs as` < n∧ψ, thus bounding the model length of the formula to at most n−1.
As referenced in [ZH04], Skakkebæk et al. have used a reduction from the problem of determining emptiness of star-free regluar languages to deciding validity of DC formulas to prove the non-elementariness of DC validity checking, due to negations. We note that more specifically, it is chop below negation that causes this blow-up, because in the other cases, we can simply rewrite the formula to a negation normal form1.
We will show how a bound on the model length can be determined forany DC formula that does not contain unguarded chop below negation. In Figure 5.1 on the next page, we have specified an algorithm findkfor calculating the bound kon the model length of a formulaφwhile checking that it belongs to this class of formulas. Otherwise, an error will be raised. The algorithm shall assume that the formula has already been rewritten to NNF.
Thefindk function, which only takesφas its parameter, uses an auxiliary recursive functionfindk’that returns a triple (k,reqG,isG). kis of course the bound on the model length that we are looking for, while reqG is a boolean value that indicates if φ requires a guard, i.e. it contains an unguarded chop below negation. isG is a boolean value that is true if and only if φis (a con-junction containing) a formula` < n. Thefindkfunction can only returnk if findk’(φ,false) returnedreqG =false.
Most of the algorithm is quite straightforward. However, a few points must
1Recall that with discrete time, negated duration formulas, ¬R
S ≥nare equivalent to RS≤n−1
CHAPTER 5. MODELS OF ELEMENTARY LENGTH
Findk(φ)
function findk’(φ)
ifφ=trueorφ=false then return (0,false,false) else ifφ=R
S≥n
then return (n,false,false) else ifφ=¬ψ
then ifψ=R S≥n
then return (n−1,false, S=true) else ifψ=ψ1_ψ2
then return (0, true,false) else raise error (* Not in NNF*) else ifφ=φ1∧φ2
then let (k1,reqG1,isG1) =findk’(φ1) (k2,reqG2,isG2) =findk’(φ2) in if isG1 andisG2
then return (min(k1, k2),false, true) else ifisG1
then return (k1,false, true) else ifisG2
then return (k2,false, true)
else return (k1+k2,reqG1∨reqG2,false) end
else ifφ=φ1∨φ2
then let (k1,reqG1,isG1) =findk’(φ1) (k2,reqG2,isG2) =findk’(φ2)
in return (max(k1, k2),reqG1∨reqG2,isG1∧isG2) end
else (*φ=φ1_φ2 *)
let (k1,reqG1,isG1) =findk’(φ1) (k2,reqG2,isG2) =findk’(φ2) in return (k1+k2,reqG1∨reqG2,false) end
endfindk’
let (k,reqG,isG) =findk’(φ) in ifreqG
then raise error (* Unguarded chop below negation *) else returnk
end
Figure 5.1: An algorithm for finding k, the bound on the model length, while checking that φdoes not contain chop below negation.
CHAPTER 5. MODELS OF ELEMENTARY LENGTH be made:
• If findk’ encounters a negation, and the operand of that negation is a chop, it returns (0, true, f alse), i.e. it requires a guard, and is not a guard itself. Thek value of 0 is arbitrarily chosen, since it will always be the required guard that bounds the model length — if no guard is present, thekvalue cannot be deduced.
• A conjunction hasisG =true if findk’ on one of its children returned isG=true. In this case, the kvalue of the conjunction is the kvalue of the child that is a guard, or the minimum of thekvalues of the children, if both are guards.
• A disjunction hasisG=true if both of its children returnedisG=true.
In this case, thekvalue is the maximum of thekvalues of the children.
• Disjunctions and chop havereqG=trueiffindk’on one of their children returnedreqG=true. Similarly for conjunctions, unlessfindk’on one of the children returnedisG=true, meaning that the child acts as a guard, hereby achieving a bound on the model length of the conjunction.
We shall conclude with a few examples of running the algorithm:
• ForR
x≥5∧R
¬x≥2 we will find k= 7.
• ForR
x≥5∧R
y≥2 we will findk= 7 even though we could have gone as small ask= 5, but we have chosen k=k1+k2 as a safe approximation, because a further analysis of the DC formulas and state assertions would quickly grow complex for larger formulas.
• Fortrue∨R
x≥5∨R
y≥2 we will findk= 5 even though the entire for-mula could have been simplified totruehavingk= 0. This indicates that it is probably a good idea to apply the DC simplifications of Section 4.2 on page 48 before running thefindkalgorithm.
• Fortrue_R
x≥5_R
y≥2 we will find k= 7.
• For¬ true_R x≥5
we will get an error, because it contains unguarded chop below negation.
• For¬ true_R x≥5
∧(` <7) we will find k= 6 because ` <7 acts as a guard.
Chapter 6
Design
In this chapter, we shall focus on splitting the functionality into packages and classes (together called themodel elements). Generally, we are trying to provide an answer to questions beginning withwhere rather thanhow, the latter being deferred to Chapter 7 on implementation (see page 62). In the following, we will describe the high-level design and give UML diagrams to provide an overview and illustrate dependencies between the model elements. First, we start by a brief introduction to the type of UML diagrams used in this chapter.
6.1 Brief UML Diagram Introduction
In a package diagram (such as the one in Figure 6.1 on the next page) the packages are represented by “folder” symbols. In a class diagram (such as the one in Figure 6.2 on page 59), classes are represented by boxes.
Arrows represent one-way associations, indicating a has-a relationship be-tween the two elements. This will typically mean that the class from which the arrow originates has a field of the type of the class to which the arrow points.
Dashed lines with arrows represent dependencies, indicating auses-a rela-tionship, which is considered a weaker relationship than an association.
The symbol indicates a boundary class, i.e. a class with an interface to the outside world. We shall use this symbol in connection with graphical user interface (GUI) classes.