package pdsreachability
Install
Dune Dependency
Authors
Maintainers
Sources
md5=e39c457a945cc4c42953502a1e56f14b
sha512=325e3e7f6eae417d4452e65360eeb756fc68f93bb4b842f2b2b5c9d02416e4e7c00f96b6f0ac051b287b7bf42a99cdab32188f64eaa7d9d424ade6567816d323
Description
This library performs efficient reachability queries on abstractly specified pushdown systems.
Published: 18 Oct 2023
README
pdsreachability
This repository contains a library which can be used to perform reachability queries on large, abstractlyspecified pushdown systems. (Reachability in a PDS is equivalent to reachability in a PDA.) These reachability queries are performed by empty stack: rather than explicitly specifying accepting states, any state which can be reached with an empty stack is considered to accept.
The user of this library provides a basis module defining how transitions are computed from states and arriving stack elements; the library provides an interface by which the states reachable from a given start state and stack. If the basis module's operations are computable and the state and stack grammars are finite, then reachability is decidable and so this library will always produce an answer in finite time.
For examples of use, please see the unit tests in the test/test_reachability.ml
file.
Installing
This library can be installed via OPAM.
Building
This project uses Dune as a build tool. After cloning this repository, it should be sufficient to perform the following steps:
Install dependencies.
`opam install jbuilder batteries jhupllib monadlib ocamlmonadic ppx_deriving ppx_deriving_yojson yojson`
Build the project.
`make && make test`
Performance Foci
This library aims to answer reachability queries quickly even on very large pushdown systems. The following points were taken into consideration in pursuit of this goal:
The user specifies how transitions may be computed for each state and arriving stack element and generally does not add states or transitions directly. The library will construct only the part of the PDS necessary to answer the presented reachability questions.
The transitions themselves are abstracted via "dynamic pop" functions. A "dynamic pop" edge is permitted to compute how a transition should proceed based upon the top element of the stack. This is useful, for instance, to encode a step which checks that the top element of the stack is not a particular value: rather than enumerating stack elements which may be popped and then repushed, a single dynamic pop can address all of these cases.
The reachability analysis can reuse the information it gathers over multiple queries. The same query performed on the same structure twice will, the second time it is made, take on the order of constant time to answer. Queries which rely upon similar proofs or otherwise overlap in their reachability closure can share work.
Dependencies (9)

yojson
>= "1.7.0"

ppx_deriving_yojson
>= "2.1"

ppx_deriving
>= "3.2"

ocamlmonadic
>= "0.4.1"

jhupllib
>= "0.3"

dune
>= "1.4"

batteries
>= "3.0"
 basethreads

ocaml
>= "4.08.0"
Dev Dependencies (1)

ounit
withtest
Used by
None
Conflicts
None