Decision problems for pushdown threads

Threads as contained in a thread algebra emerge from the behavioral abstraction from programs in an appropriate program algebra. Threads may make use of services such as stacks, and a thread using a single stack is called a pushdown thread. Equivalence of pushdown threads is shown decidable whereas pushdown thread inclusion is undecidable. This is again an example of a borderline crossing where the equivalence problem is decidable, whereas the inclusion problem is not.

• Type: Journal
• Year: 2007
• Where: ACTA
• Authors: Jan A. Bergstra, Inge Bethke, Alban Ponse
• Keywords: ACTA 2007, Appropriate Program Algebra, Pushdown Thread, Threads