Symbolic Representations of Kripke Structures and Automata

This tool draws the state transition diagram of a Kripke structure or a finite state automaton for you that is given in terms of a symbolic description (propositional formulas). It is assumed that next(q) denotes the next value of a state variable q. The automaton may be nondeterministic, and it is allowed that all variables are state variables (which denotes then a Kripke structure rather than an automaton).

The tool can also compute symbolically predecessor and successor states of a given set of states (also given symbolically as a propositional formula). Further examples taken from previous exams are also available.