Prove that determining if a PDA has an infinite language is decidable

Question

I have been given the following problem and was wondering if my solution is correct (taken from the textbook exercise in the book Introduction to the Theory of Computation by Martin Sipser): Given $$\text{INFINITE}_{\text{PDA}} =\{\langle M\rangle \mid M\text{ is a PDA }\text{and L(M) is infinite}\}$$

Prove that $\text{INFINITE}_{\text{PDA}}$ is decidable.

The following is my solution:

On input <M>:
1. Repeat until there are transitions:
   a. Mark current state and delete the transition that moved you to the state
   b. If an already marked state is reached, accept
2. If no other transition exists, reject

Can this be considered a valid solution? I think the fact that we are checking if a cycle exists in the PDA is sufficient to prove that the language is infinite am I correct? I believe there could be a PDA that has a loop in a non-accepting branch of the computation and my algorithm would still say it has an infinite language which is wrong, am I correct?

Answer 1

I'm not sure whether I understood your solution right. Here is my suggestion:

For code of M:

1- Find all paths from start state to an accept state which every state occurs only once.

2- Check whether in states that occurs in paths, There are states that are connected together with a path which doesn't appear in the main path from start state to accept state?

If there are, accept. OTHERWISE, reject.

With this algorithm, If the language is infinite, Then there are definitely states and strings that transition function allows a loop with them. If it doesn't, Since M has finite number of states, There are only finitely many strings which are accepted by M.

Also since we just look for paths from start state to accept stats that each state appears at most once, We won't have any loop in performance of this algorithm. Because there are only finite paths that satisfy this requirement.