Dragan Bosnacki: Analysis of a Boolean Model for Rheumatoid Arthritis Using SMTSolvers

Event Details

Rheumatoid Arthritis (RA) is an autoimmune disease that affects about
one percent of the world population. A medicine for RA has not yet been
found, current treatment options only decelerating the progress of the
disease. In this work a Boolean network model for RA is analysed. Two
kinds of models, synchronous and asynchronous are compared. Attractors
in the state space of the models are identified that correspond to the
steady states and stable cycles of the network. To this end
Satisfiability Modulo Theory (SMT) solvers and an adaptation of the
Tarjan’s algorithm for finding strongly connected components in a graph
are used for the synchronous and asynchronous models, respectively.  By
analysing the stability of the network nodes potential drug targets are
identified. The results show a significant overlap with similar findings
in the literature which indicates that the Boolean networks can be a
feasible approach for identifying biomarkers and drug targets.