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

868 questions

986 answers


438 users

0 votes

Exam : 06.09.2016 : Q8 d : (

Q1. How universal automata got converted to existential directly ? Could you also please share the conditions for translating an universal automata to existential ?

Q2. As the remarks mentioned there that the first automata is not totally defined and thatswhy we can't easily obtain LTL by boolean operations on omega-automata. It looks like both automata got translated to LTL and just ORed. Could you please explain how final result ended in Ga | !p ? 

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

1 Answer

0 votes
Universal automata are typically converted to existential ones by determinizing the automaton. In the case you mention, the automaton has only one state with a self-loop, so that every word has exactly one run. Hence, that automaton is already deterministic, so that it does not matter whether we consider it as a universal or existential one. Its unique run must be accepting.

The comment in the example solution is maybe not that comprehensive. It wants to say that we cannot easily compute the disjunction by means of a product automaton, so we don't try this and translate both automata to LTL first and then to LO2. You can, of course, also directly translate them to LO2 without translating to LTL as an intermediate step.

For the translation to LTL, note that the first automaton has only a single state with a self-loop labeled with "a", so that only the word where always "a" holds has a run at all. Certainly, that run also satisfies the acceptance condition, and therefore the first automaton is equivalent to Ga. The second automaton accepts any word that starts with !p.

From the LTL formula to LO1 (which is a subset of LO2) is then straightforward.
by (139k points)
Imprint | Privacy Policy