Abstract:
Model checking is a useful method to verify automatically the correctness of a system. Many systems of interest are open: their behaviour depends on the interaction with an external environment.
To address properly the verification of open systems, a new technique, named module checking, has been introduced and intensively studied in the literature.
In this talk, we first recall the basic concepts and the main results regarding finite-state module checking. Then, we focus on open pushdown systems and introduce the pushdown module checking problem.
We show that, in the perfect information setting, the CTL and µ-calculus pushdown module checking problem is 2Exptime-complete, while it is 3Exptime-complete with respect to CTL* formulas. In particular, we show that, for a fixed formula, the problem is Exptime-complete. On the other hand, in the imperfect information setting, the problem becomes undecidable when the environment has imperfect information about the pushdown store.
We conclude the talk by considering restricted open pushdown models in which it is possible, for fixed formulas, to solve the pushdown module checking problem in polynomial time.
Bio:
Aniello Murano is an Associate Professor in Computer Science at the Università di Napoli Federico II, since November 2010. He joined this university in March 2005 as an Assistant Professor. He got the PhD in
Computer Science in February 2003 at the Università di Salerno, working under the supervision of Margherita Napoli, Salvatore La Torre, and Moshe Y. Vardi. Form October 2002 until March 2005 he has been a temporary researcher at the Università degli Studi di Salerno. During this period he has been a one-year Post-Doctoral Researcher at the Hebrew University of Jerusalem, working under the supervision of Orna Kupferman. In January 2010 he has been awarded with Orna Kupferman of the biennal Vigevani research prize.