Summary: We address the model checking problem of omega-regular linear-time properties for shared memory concurrent programs modeled as multi-pushdown systems. We consider here boolean programs with a finite number of threads and recursive procedures. It is well-known that the model checking problem is undecidable for this class of programs. In this paper, we investigate the decidability and the complexity of this problem under the assumption of scope-boundedness defined recently by S. La Torre and M. Napoli [Lect. Notes Comput. Sci. 6901, 203–218 (2011; Zbl 1343.68172)]. A computation is scope-bounded if each pair of call and return events of a procedure executed by some thread must be separated by a bounded number of context-switches of that thread. The concept of scope-bounding generalizes the one of context-bounding [S. Qadeer and J. Rehof, Lect. Notes Comput. Sci. 3440, 93–107 (2005; Zbl 1087.68598)] since it allows an unbounded number of context switches. Moreover, while context-bounding is adequate for reasoning about safety properties, scope-bounding is more suitable for reasoning about liveness properties that must be checked over infinite computations. It has been shown in [La Torre and Napoli, loc. cit.] that the reachability problem for multi-pushdown systems under scope-bounding is PSPACE-complete. We prove in this paper that model-checking linear-time properties under scope-bounding is also decidable and is EXPTIME-complete.
For the entire collection see [Zbl 1251.68006].