The Sigali Tool Box Environment

Sigali is a tool that offers functionalities for verification of reactive systems and discrete controller synthesis. It manipulates ILTS: Implicit Labeled Transition Systems, an equational and symbolic representation of automata. The techniques used consist in manipulating the system of equations modeling the system instead of the sets of solutions, thus avoiding the enumeration of the state space. Each set of states is uniquely characterized by a predicate and the operations on sets can be equivalently performed on the associated predicates. A wide variety of properties, such as invariance, reachability and attractivity can be checked or ensured. Many algorithms for computing state predicates are also available