Sciweavers

FSTTCS
2001
Springer

Beyond Regular Model Checking

14 years 2 months ago
Beyond Regular Model Checking
Abstract. Regular Model-Checking (RMC) is a technique for the formal verification of infinite state systems based on the theory of regular languages. In the paper “Beyond Regular Model Checking” Fisman and Pnueli have shown that RMC can be extended to languages accepted by cascade products of single-state deterministic pushdown automata and finite automata. In this paper we further extend RMC to arbitrary deterministic context-free languages. For this purpose, and inspired by recent results of Caucal, we introduce height-deterministic pushdown automata and show that they satisfy adequate closure properties.
Dana Fisman, Amir Pnueli
Added 28 Jul 2010
Updated 28 Jul 2010
Type Conference
Year 2001
Where FSTTCS
Authors Dana Fisman, Amir Pnueli
Comments (0)