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.

• Type: Conference
• Year: 2001
• Where: FSTTCS
• Authors: Dana Fisman, Amir Pnueli
• Keywords: Deterministic Pushdown Automata, FSTTCS 2001, Height-deterministic Pushdown Automata, Pushdown Automata, Software Engineering