Minimization of visibly pushdown automata using partial Max-SAT

DOI10.1007/978-3-662-54577-5_27MaRDI QIDQ3303909zbMATH OpenOpenAlexFDO

Authors Matthias Heizmann, Christian Schilling, Daniel Tischner

Publication date 5 August 2020

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1701.05160

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

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 improvements on benchmarks from the software verification competition SV-COMP.

Recommendations

• Minimizing Variants of Visibly Pushdown Automata
• scientific article; zbMATH DE number 4178795
• On Model Checking for Visibly Pushdown Automata
• Trimming visibly pushdown automata
• Visibly pushdown automata: universality and inclusion via antichains

Cites work

• A minimized automaton representation of reachable states
• Adding nesting structure to words
• Advanced automata minimization
• Automata, Languages and Programming
• Beyond Language Equivalence on Visibly Pushdown Automata
• Büchi automata can have smaller quotients
• Experimental Evaluation of Classical Automata Constructions
• Fair Simulation Relations, Parity Games, and State Space Reduction for Büchi Automata
• Forest automata for verification of heap manipulation
• scientific article; zbMATH DE number 3460178 (Why is no real title available?)
• Mediating for reduction (on minimizing alternating Büchi automata)
• Minimising deterministic Büchi automata precisely using SAT solving
• Minimization of symbolic automata
• Minimization, Learning, and Conformance Testing of Boolean Programs
• Minimizing Variants of Visibly Pushdown Automata
• Model checking procedural programs
• MONA IMPLEMENTATION SECRETS
• Nested interpolants
• On Solving the Partial MAX-SAT Problem
• Reduction of nondeterministic tree automata
• SAT-based minimization of deterministic -automata
• Trimming visibly pushdown automata
• Visibly pushdown languages
• Visibly Pushdown Transducers for Approximate Validation of Streaming XML

Cited in

(6)

• Minimizing Variants of Visibly Pushdown Automata
• Minimization of visibly pushdown automata is NP-complete
• Trimming visibly pushdown automata
• Minimization, Learning, and Conformance Testing of Boolean Programs
• Simulation relations and applications in formal methods
• Relations between equation automata and follow automata

Describes a project that uses

Uses Software

• MONA

This page was built for publication: Minimization of visibly pushdown automata using partial Max-SAT

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3303909)