Symbolic Computation of Predecessor and Successor States

This page provides a list of examples for symbolically computing the universal/existential predecessor/successor states of a set of states under a given transition relation. The examples were taken from previous exams.

Exam 2013.10.07; Problem 3a

state variables
input variables
initial states
transition relation	(next(a) <-> (a | b)) & (next(b) <-> (a & p)) & (p <-> !next(a))
state set
	existential predecessors (pre∃)
	universal predecessors (pre∀)
	existential successors (suc∃)
	universal successors (suc∀)

Exam 2013.10.07; Problem 3b

state variables
input variables
initial states
transition relation	(next(a) <-> (a | b)) & (next(b) <-> (a & p)) & (p <-> !next(a))
state set
	existential predecessors (pre∃)
	universal predecessors (pre∀)
	existential successors (suc∃)
	universal successors (suc∀)

Exam 2013.07.22; Problem 4b

state variables
input variables
initial states
transition relation	(p<->(a & next(p))) & (q & (b & next(q)))
state set
	existential predecessors (pre∃)
	universal predecessors (pre∀)
	existential successors (suc∃)
	universal successors (suc∀)

Exam 2013.07.22; Problem 4c

state variables
input variables
initial states
transition relation	(p<->(a & next(p))) & (q & (b & next(q)))
state set
	existential predecessors (pre∃)
	universal predecessors (pre∀)
	existential successors (suc∃)
	universal successors (suc∀)

Exam 2012.03.19; Problem 3a

state variables
input variables
initial states
transition relation	(next(a) <-> !a) & (next(b) <-> (a ^ b)) & (p ^ a)
state set
	existential predecessors (pre∃)
	universal predecessors (pre∀)
	existential successors (suc∃)
	universal successors (suc∀)

Exam 2012.03.19; Problem 3b

state variables
input variables
initial states
transition relation	(next(a) <-> !a) & (next(b) <-> (a ^ b)) & (p ^ a)
state set
	existential predecessors (pre∃)
	universal predecessors (pre∀)
	existential successors (suc∃)
	universal successors (suc∀)

Exam 2012.02.13; Problem 4a

state variables
input variables
initial states
transition relation	(p ^ q) & (next(p) ^ next(q)) & (next(p) <-> a)
state set
	existential predecessors (pre∃)
	universal predecessors (pre∀)
	existential successors (suc∃)
	universal successors (suc∀)

Exam 2012.02.13; Problem 4b

state variables
input variables
initial states
transition relation	(p ^ q) & (next(p) ^ next(q)) & (next(p) <-> a)
state set
	existential predecessors (pre∃)
	universal predecessors (pre∀)
	existential successors (suc∃)
	universal successors (suc∀)

Exam 2010.12.08; Problem 4c

state variables
input variables
initial states
transition relation	(p -> a & next(p)) & (q <-> !a | a & next(q)) & !(!next(q) & !next(p) & !next(a))
state set
	existential predecessors (pre∃)
	universal predecessors (pre∀)
	existential successors (suc∃)
	universal successors (suc∀)

Exam 2010.12.08; Problem 4d

state variables
input variables
initial states
transition relation	!next(a))
state set
	existential predecessors (pre∃)
	universal predecessors (pre∀)
	existential successors (suc∃)
	universal successors (suc∀)

Exam 2010.09.23; Problem 4a

state variables
input variables
initial states
transition relation	(p -> a & next(p)) & (q <-> !a | a & next(q)) & !(!next(q) & !next(p) & !next(a))
state set
	existential predecessors (pre∃)
	universal predecessors (pre∀)
	existential successors (suc∃)
	universal successors (suc∀)

Exam 2010.09.23; Problem 4b

state variables
input variables
initial states
transition relation	(p -> a & next(p)) & (q <-> !a | a & next(q)) & !(!next(q) & !next(p) & !next(a))
state set
	existential predecessors (pre∃)
	universal predecessors (pre∀)
	existential successors (suc∃)
	universal successors (suc∀)

Exam 2010.09.23; Problem 4c

state variables
input variables
initial states
transition relation	(p -> a & next(p)) & (q <-> !a | a & next(q)) & !(!next(q) & !next(p) & !next(a))
state set
	existential predecessors (pre∃)
	universal predecessors (pre∀)
	existential successors (suc∃)
	universal successors (suc∀)

Exam 2010.09.23; Problem 4d

state variables
input variables
initial states
transition relation	(p -> a & next(p)) & (q <-> !a | a & next(q)) & !(!next(q) & !next(p) & !next(a))
state set
	existential predecessors (pre∃)
	universal predecessors (pre∀)
	existential successors (suc∃)
	universal successors (suc∀)

Exam 2010.07.23; Problem 3a

state variables
input variables
initial states
transition relation	(p ^ q) & (next(p) ^ next(q)) & (next(p) <-> a)
state set
	existential predecessors (pre∃)
	universal predecessors (pre∀)
	existential successors (suc∃)
	universal successors (suc∀)

Exam 2010.07.23; Problem 3b

state variables
input variables
initial states
transition relation	(p ^ q) & (next(p) ^ next(q)) & (next(p) <-> a)
state set
	existential predecessors (pre∃)
	universal predecessors (pre∀)
	existential successors (suc∃)
	universal successors (suc∀)