Formally Verified Compositional Algorithms for Factored Transition Systems

Abstract

Artificial Intelligence (AI) planning and model checking are two disciplines that found wide practical applications. It is often the case that a problem in those two fields concerns a transition system whose behaviour can be encoded in a digraph that models the system's state space. However, due to the very large size of state spaces of realistic systems, they are compactly represented as propositionally factored transition systems. These representations have the advantage of being exponentially smaller than the state space of the represented system. Many problems in AI~planning and model checking involve questions about state spaces, which correspond to graph theoretic questions on digraphs modelling the state spaces. However, existing techniques to answer those graph theoretic questions effectively require, in the worst case, constructing the digraph that models the state space, by expanding the propositionally factored representation of the system. This is not practical, if not impossible, in many cases because of the state space size compared to the factored representation. One common approach that is used to avoid constructing the state space is the compositional approach, where only smaller abstractions of the system at hand are processed and the given problem (e.g. reachability) is solved for them. Then, a solution for the problem on the concrete system is derived from the solutions of the problem on the abstract systems. The motivation of this approach is that, in the worst case, one need only construct the state spaces of the abstractions which can be exponentially smaller than the state space of the concrete system. We study the application of the compositional approach to two fundamental problems on transition systems: upper-bounding the topological properties (e.g. the largest distance between any two states, i.e. the diameter) of the state spa ce, and computing reachability between states. We provide new compositional algorithms to solve both problems by exploiting different structures of the given system. In addition to the use of an existing abstraction (usually referred to as projection) based on removing state space variables, we develop two new abstractions for use within our compositional algorithms. One of the new abstractions is also based on state variables, while the other is based on assignments to state variables. We theoretically and experimentally show that our new compositional algorithms improve the state-of-the-art in solving both problems, upper-bounding state space topological parameters and reachability. We designed the algorithms as well as formally verified them with the aid of an interactive theorem prover. This is the first application that we are aware of, for such a theorem prover based methodology to the design of new algorithms in either AI~planning or model checking.