Dynamic Pushdown Networks (DPNs) are a model for multithreaded programs with recursion and dynamic creation of threads. In this paper, we propose a temporal logic called NTL for reasoning about the call- and return- as well as thread creation behaviour of DPNs. Using tree automata techniques, we investigate the model checking problem for the novel logic and show that its complexity is not higher than that of LTL model checking against pushdown systems despite a more expressive logic and a more powerful system model. The same holds true for the satisfiability problem when compared to the satisfiability problem for a related logic for reasoning about the call- and return-behaviour of pushdown systems. Overall, this novel logic offers a promising approach for the verification of recursive programs with dynamic thread creation.

翻译：动态下推网络（DPN）是一种用于建模具有递归和动态线程创建的多线程程序的模型。本文提出一种名为NTL的时态逻辑，用于推理DPN中的调用与返回行为以及线程创建行为。采用树自动机技术，我们研究了这一新型逻辑的模型检测问题，并证明尽管该逻辑表达能力更强且系统模型更强大，其复杂度并不高于针对下推系统的LTL模型检测。与用于推理下推系统调用与返回行为的相关逻辑的可满足性问题相比，该逻辑的可满足性问题复杂度同样未增加。总体而言，这一新型逻辑为验证具有动态线程创建的递归程序提供了一种有前景的方法。