Sigali is a model-checking tool-based which manipulates ILTS: Implicit Labeled Transition Systems (which can be seen as an equational representation of an automaton) as intermediate models for discrete event systems. It offers functionalities for verification of reactive systems and discrete controller synthesis. It is developed jointly by Espresso and Vertecs. Sigali is a tool box that manipulates (sets of) variables and predicates by means of (predefined) functions using a Mathematica-based language. Using Sigali, one can create predicates over a set of variables. There exists functions to manipulate them (intersection, union, complementary, test of inclusion, etc). Some functions are used to replace some variables in a predicate by other predicates. All these operations are extended to the manipulation of lists of predicates. Sigali also manipulates cost functions. These are functions that associate to each solution of a predicate a given integer value. These cost functions can be build by associating to each variable a given cost according to the value of the variable. Starting from the existing functions, it is also possible to define new functions, allowing, from example, to have libraries of functions dedicated to controller synthesis, optimal control or verification. Of course, one can also manipulate ILTS (e.g. to compose them according to different composition operators). Functions allowing to compute the successors (resp. predecessors, etc) belongs to the function kernel of Sigali. They can be further used to implement more intricate functions as the ones that compute the set of reachable states, the set of states that can reach a set of states by triggering uncontrollable events, etc.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element