Fusion Logic augments conventional Propositional Temporal Logic (PTL) with the fusion operator. Note: the fusion-operator is basically a “chop” that does not have an explicit negation on the left hand (for right fusion logic) side (as fusion expression) or the right hand (for left fusion logic). The negation is implicit, i.e., the negation is a derived fusion expression operator. The expressiveness of Fusion Logic is the same as Propositional Interval Temporal Logic. The main differences concern computational complexity, naturalness of expression for analytical purposes, and succinctness. Fusion Logic is closely related to Propositional Dynamic Logic (PDL).
We have implemented above decision procedure for Fusion Logic in Tcl/Tk and the CUDD BDD library. The tool allows one to check the validity or satisfiability of a Fusion Logic formula. If a formula is not valid it will produce a counter example and if a formula is satisfiable it will produce an example model. Figure 4 gives a screen dump of our tool which is available at
FLCHECK version 1.2 (released 22/05/2015).
Main Changes:
FLCHECK version 1.1 (released 04/07/2013).
Main Changes:
FLCHECK version 1.0 (released 23/01/2013).
Main Changes:
FLCHECK version 0.9 (released 21/02/2012).
Main Changes:
FLCHECK version 0.8 (released 26/03/2010).
Initial release.