How Do You Create a Buchi Automaton for Specific Logical Conditions?

[dork]

--------------------------------------------------------------------------------

1. Homework Statement

Give a buchi automaton that accepts the following property
either p is true forever, or p is true until q becomes true

2. Homework Equations

check my answer if its right and correct if wrong


3. The Attempt at a Solution

Three states.
S0, S1 AND S2.
S1 AND S2 ACCEPT STATES
FROM S0 TO S1 IF IT IS P AND NOT Q . FROM S1 TO S2 IF IT IS( P NOT Q) OR (NOT P AND Q)

FROM S0 TO S2 IF IT IS P AND Q .
ON S1 IT LOOPS IF IT IS P AND NOT Q.
S2 LOOPS FOR EVERYTHING
S0 Is The Start State

Hope I Solved Everything Right.please Correct Me

 

[nate808]

If I'm Wrong

I would like to provide some feedback and clarification on your solution.

Firstly, your solution is close but there are a few errors. The states should be labeled as S0, S1, and S2, but the transitions should be labeled as P and Q instead of P and NOT Q. This is because the automaton should accept P until Q becomes true, not accept P forever unless Q becomes true.

Additionally, the transition from S0 to S2 should be labeled as NOT P and Q, not P and Q. This is because the automaton should also accept if P is not true and Q becomes true.

Furthermore, your solution does not account for the possibility of P being true and Q never becoming true. In this case, the automaton should still accept since P is true forever.

Lastly, it would be helpful to include a final state where the automaton can accept if P is true forever or if P is true until Q becomes true.

Here is a revised solution:

States: S0, S1, S2, and S3 (final state)

Transitions:
- S0 to S1 labeled as P
- S1 to S2 labeled as NOT Q
- S1 to S3 labeled as P and Q
- S2 to S3 labeled as P

This solution covers all possible scenarios and ensures that the automaton accepts the desired property. I hope this helps and please let me know if you have any further questions.

 

[Architeuthis Dux]

If I Am Wrong

Your solution looks correct to me. Great job! Just to clarify, the states S1 and S2 should both be accepting states as they represent the property being true until q becomes true. Other than that, your solution seems to fit the given property perfectly. Keep up the good work!