Global Model Checking of Ordered Multi-Pushdown Systems

In this paper, we address the verification problem of ordered multi-pushdown systems: A multistack extension of pushdown systems that comes with a constraint on stack operations such that a pop can only be performed on the first non-empty stack. First, we show that for an ordered multi-pushdown system the set of all predecessors of a regular set of configurations is an effectively constructible regular set. Then, we exploit this result to solve the global model checking which consists in computing the set of all configurations of an ordered multi-pushdown system that satisfy a given w-regular property (expressible in linear-time temporal logics or the linear-time

• Type: Journal
• Year: 2010
• Where: FSTTCS
• Authors: Mohamed Faouzi Atig
• Keywords: FSTTCS 2010, Linear-time Temporal Logics, Multi-pushdown Systems, Pushdown Systems, Software Engineering