Embedded Systems Group (ES)

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.

state variables
input variables
initial states
transition relation
state set
existential predecessors (pre∃)
universal predecessors (pre∀)
existential successors (suc∃)
universal successors (suc∀)
weakest and strongest induction lemmata (for AG phi)
weakest and strongest induction lemmata (for EG phi)