Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

769 questions

886 answers

1.3k comments

424 users

0 votes

We have a FSM: =(2Vin,2Vout,φ,2Vstate,φ)A=(2Vin,2Vout,φI,2Vstate,φR), where Vin={a}Vin={a}Vout={o}Vout={o}Vstate={p,q}Vstate={p,q}φ=pqφI=p∨qφ=φR=((a->next(p)&(q|p))<->next(q))&o

How to compute the existential predecessors of !(q->a) step by step?

in * TF "Emb. Sys. and Rob." by (120 points)

1 Answer

0 votes
Using https://es.cs.uni-kl.de/tools/teaching/SymbolicStateTrans.html, you will get the following:

∃next(p).∃next(q).∃next(a).∃next(o). ((a->next(p)&(q|p))<->next(q))&o&!(next(q)->next(a))

  = ∃next(q).∃next(a).∃next(o). !(next(q)->next(a))&o&(!a<->next(q))|!(next(q)->next(a))&o&((a->p|q)<->next(q))

  = ∃next(a).∃next(o).!next(a)&o&!a|!next(a)&o&(a->p|q)

  = ∃next(o).o&!a|o&(a->p|q)

  = o&!a|o&(a->p|q)

Remember the definition of the boolean quantification, and in many cases, one of the cofactor becomes trivial.
by (117k points)
Imprint | Privacy Policy
...