Model checking is a useful method to verify automatically the correctness of a system with respect to a desired behavior, by checking whether a mathematical model of the system satisfies a formal specification of this behavior. Many systems of interest are open, in the sense that their behavior depends on the interaction with their environment. The model checking problem for finite state open systems (called module checking) has been intensively studied in the literature. In this paper, we focus on open pushdown systems and we study the related model checking problem (pushdown module checking, for short) with respect to properties expressed by CTL and CTL* formulas. We show that pushdown module checking against CTL (resp., CTL*) is 2Exptime-complete (resp., 3Exptime-complete). Moreover, we prove that for a fixed CTL* formula, the problem is Exptime-complete.
Pushdown Module Checking
BOZZELLI, LAURA;
2005-01-01
Abstract
Model checking is a useful method to verify automatically the correctness of a system with respect to a desired behavior, by checking whether a mathematical model of the system satisfies a formal specification of this behavior. Many systems of interest are open, in the sense that their behavior depends on the interaction with their environment. The model checking problem for finite state open systems (called module checking) has been intensively studied in the literature. In this paper, we focus on open pushdown systems and we study the related model checking problem (pushdown module checking, for short) with respect to properties expressed by CTL and CTL* formulas. We show that pushdown module checking against CTL (resp., CTL*) is 2Exptime-complete (resp., 3Exptime-complete). Moreover, we prove that for a fixed CTL* formula, the problem is Exptime-complete.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
