Heuristics for ROSA’s LTS searching

Abstract

The authors have been aimed by the goal of reducing the computational cost of searching the Labeled Transition Systems, LTSs, generated by Process Algebras. In particular, we have been following the idea of moving the order of the computational cost required to find/reach a desired node/state from the exponential of the classical Breadth-First Search fashion to the polynomial produced either by the Depth-First Search or by the A∗ algorithm [6]. As usual, they both take as size of the problem the branching factor of the LTS. This paper, first, presents the Normal Formed ROSA processes required to, second, define a sound topological structure over this Process Algebra. The underlying notion of distance from this topology can be taken as the heuristics to guide the search for whatever node which reachability want to be studied, by means of an A∗ algorithm.