   
 4 Decision Procedure for Fusion Logic
4.1 Time Reversal StepTransform a left fusion formula into a right fusion logic formula.
Rules to rewrite left fusion logic formulae into right fusion logic formulae The following holds
4.2 Reduction StepTransform right fusion logic formula into an equivalent reduced form where
Let and denote non state formulae and a state formula then the definition of Transition formula is as follows: For
So only the and case will introduce a dependent variable. Let and denote non state formulae and a state formula then the definition of state formula is as follows: For Reduction function for is a bit more involved because could be valid for intervals with only one state. Solution: a function is introduced which transforms an arbitrary fusion expression into another formula such that holds. Note: holds. The following holds
Given a right fusion logic formula The Reduction Step yields: where and . The corresponding invariant is
4.3 BDD StepTransform into BDD based satisfiability problem.
Let us examine the ‘Always’ operator We know that invariant only contains (next) as temporal operator. So it can only constrain the first two states of each suffix interval. Introducing BDDs ’s:
Given right fusion logic formula With and corresponding invariant: Then and
and Encoding as a BDDbased satisfiability problem:
To construct a satisfying interval (in case is satisfiable) we proceed as follows. Let be that set of states for which is true.
Implementation of decision procedure
  

 