Reachability for Finite-state Process Algebras Using Horn Clauses

Nataliya Skrypnyuk, Flemming Nielson

Research output: Contribution to journalJournal articleResearchpeer-review


In this work we present an algorithm for solving the reachability problem in finite systems that are modelled with process algebras. Our method is based on Static Analysis, in particular, Data Flow Analysis, of the syntax of a process algebraic system with multi-way synchronisation. The results of the Data Flow Analysis are used in order to build a set of Horn clauses whose least model corresponds to an overapproximation of the reachable states. The computed model can be refined after each transition, and the algorithm runs until either a state whose reachability should be checked is encountered or it is not in the least model for all constructed states and thus is definitely unreachable. The advantages of the algorithm are that in many cases only a part of the Labelled Transition System will be built which leads to lower time and memory consumption. Also, it is not necessary to save all the encountered states which leads to further reduction of the memory requirements of the algorithm.
Original languageEnglish
JournalInternational Journal of Foundations of Computer Science
Issue number2
Pages (from-to)283-302
Publication statusPublished - 2013

Fingerprint Dive into the research topics of 'Reachability for Finite-state Process Algebras Using Horn Clauses'. Together they form a unique fingerprint.

Cite this