2015/11/03 by Heußner, Alexander
paper · doi:10.14279/tuj.eceasst.47.725
The formal model of recursive communicating processes (RCPS) is important in practice but does not allows to derive decidability results for model checking questions easily. We focus a partial order representation of RCPS’s execution by graphs—so called run graphs, and suggest an underapproximative verification approach based on a bounded-treewidth requirement. This allows to directly derive positive decidability results for MSO model checking (seen as partial order logic on run graphs) based on a context-freeness argument for restricted classes run graph.