Reachability of Patterned Conditional Pushdown Systems
Xin Li, Patrick Gardy, Yu-Xin Deng, and Hiroyuki Seki
Conditional pushdown systems (CPDSs) extend pushdown systems by associating each
transition rule with a regular language over the stack alphabet. The goal is to
model program verification problems that need to examine the runtime call stack
of programs. Examples include security property checking of programs with stack
inspection, compatibility checking of HTML5 parser specifications, etc.
Esparza et al. proved that the reachability problem of CPDSs is EXPTIME-complete,
which prevents the existence of an algorithm tractable for all instances in general.
Driven by the practical applications of CPDSs, we study the reachability of
patterned CPDS (pCPDS) that is a practically important subclass of CPDS, in which
each transition rule carries a regular expression obeying certain patterns.
First, we present new saturation algorithms for solving state and configuration
reachability of pCPDSs. The algorithms exhibit the exponential-time complexity
in the size of atomic patterns in the worst case. Next, we show that the reachability
of pCPDSs carrying simple patterns is solvable in fixed-parameter polynomial time and
space. This answers the question on whether there exist tractable reachability analysis
algorithms of CPDSs tailored for those practical instances that admit efficient
solutions such as stack inspection without exception handling. We have evaluated
the proposed approach, and our experiments show that the pattern-driven algorithm
steadily scales on pCPDSs with simple patterns.