Minimization of Visibly Pushdown Automata Using Partial Max-SAT
Matthias Heizmann, Christian Schilling, Daniel Tischner
TL;DR
This paper introduces a novel method for reducing the state space of visibly pushdown automata using partial Max-SAT encoding, leading to more efficient automata-based software verification.
Contribution
It defines a new equivalence relation for VPA state merging and encodes it as a PMax-SAT problem, enabling effective state reduction.
Findings
Significant state reduction achieved in VPA.
Improved performance in software verification benchmarks.
Efficient PMax-SAT based algorithm for automata minimization.
Abstract
We consider the problem of state-space reduction for nondeterministic weakly-hierarchical visibly pushdown automata (VPA). VPA recognize a robust and algorithmically tractable fragment of context-free languages that is natural for modeling programs. We define an equivalence relation that is sufficient for language-preserving quotienting of VPA. Our definition allows to merge states that have different behavior, as long as they show the same behavior for reachable equivalent stacks. We encode the existence of such a relation as a Boolean partial maximum satisfiability (PMax-SAT) problem and present an algorithm that quickly finds satisfying assignments. These assignments are sub-optimal solutions to the PMax-SAT problem but can still lead to a significant reduction of states. We integrated our method in the automata-based software verifier Ultimate Automizer and show performance…
Click any figure to enlarge with its caption.
Figure 1
Figure 2
Figure 3
Figure 4
Figure 5
Figure 6
Figure 7
Figure 8
Figure 9
Figure 10
Figure 11
Figure 12
Figure 13
Figure 14
Figure 15Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.