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

1.1k questions

1.3k answers

1.7k comments

557 users

0 votes

I got the idea of doing Fb=AFb from a solution given for a problem in 2020.02.19 exam question(Problem 8: Translation between different logics)

does it mean that it can be done only while solving this kind of problem?

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

2 Answers

+2 votes
 
Best answer
Fb is not equivalent to AFb; the former is a path formula, the latter is a state formula. However, AXphi is equivalent to AXAphi, and therefore AXFb is equivalent to AXAFb. So, it is the context to be after an AX that makes Fb and AFb the same, without that context, it may not be the case.

Look, x is also not equivalent to x&y, but when I am considering y -> x&y, and can replace x&y by y since the context excludes all counterexamples. That is comparable to the above situation; and still x&y is not equivalent to x.
by (170k points)
selected by
+1 vote
The task of the the question you are citing is clearly to transform the formulas in order convert them to different logic classes.

In other tasks, you are asked to perform a defined procedure on a given formula, not on an equivalent one. The reason is that these procedures work syntactically.

But I think your question is not only whether it is allowed to convert a formula but what conversions are correct.

On the formulas you marked, you can see that they have an outer universal path quantifier (A). It contains the next operator (X) and the eventually operator (F).

The path quantifier A means “take all infinite paths from here, check whether following properties hold on these paths”. Hence, the outer quantifiers AG lead to a check whether every reachable (on an infinite path) state satisfies the inner property XFb on every path going through them.

One more example, the formula AGFb and AGAFb are equivalent. However, AFGb is different from AFAGb. Think of a structure looking like ↻{b}→{}→{b}↺ with self loops at the outer states. The left state is the initial state. There is a path looping in the left state, all other paths leave this state after a while and loop in the right state. The path that loops in the left state is the counterexample that tells the two formulas apart. It satisfies FGb. After finite time (even zero steps), it satisfies Gb. It does not satisfy FAGb. It stays in the same state. No matter how long we wait, we'd always need to evaluate AGb in this first state. It just doesn't hold as all paths also includes the paths leaving this state.

A totally different example from a different domain:

0*3 = 0*5 but you may not conclude 3=5 although 3 was replaced by 5 here.
by (25.6k points)
Imprint | Privacy Policy
...