Email Gateway (Nov 17 2023 at 10:03): Email Gateway (Nov 17 2023 at 10:03):From: Peter Lammich <lammich@in.tum.de>
Enjoy two new entries on Labeled Transition Systems, and Pushdown
Systems, verifying the important post, pre, and dual* algorithms for
reachability in PDSs!
Labeled Transition Systems
Labeled transition systems are ubiquitous in computer science. They are
used e.g. for automata and for program graphs in program analysis. We
formalize labeled transition systems with and without epsilon
transitions. The main difference between formalizations of labeled
transition systems is in their choice of how to represent the transition
system. In the present formalization the set of nodes is a type, and a
labeled transition system is represented as a locale fixing a set of
transitions where each transition is a triple of respectively a start
node, a label and an end node. Wimmer [Wim20] provides an overview of
formalizations of graphs and transition systems.
Pushdown Systems
We formalize pushdown systems and the correctness of the pushdown
reachability algorithms post* (forward search), pre* (backward search)
and dual* (bi-directional search). For pre* we refine the algorithm to
an executable version for which one can generate code using Isabelle's
code generator. For pre* and post* we follow Stefan Schwoon's PhD thesis
[Sch02a]. The dual* algorithm is from a paper by Jensen et. al presented
at ATVA2021 [JSS+21]. The formalization is described in our FMCAD2022
paper [SSST22] in which we also document how we have used it to do
differential testing against a C++ implementation of pushdown
reachability called PDAAAL. Lammich et al. [Lam09, LMW09] formalized the
pre* algorithm for dynamic pushdown networks (DPN) which is a
generalization of pushdown systems. Our work is independent from that
because the post* of DPNs is not regular and additionally the DPN
formalization does not support epsilon transitions which we use for
post* and dual*.
Last updated: Apr 28 2024 at 16:17 UTC