Reaction systems are a formalism inspired by the functioning of living cells. They allow for specifying and analysing computational processes in which reactions operate on sets of molecules.

The behaviour of a reaction system is determined by the interactions of its reactions, which are based on the mechanisms of facilitation and inhibition. The formal treatment of reaction systems is qualitative and there is no direct representation of the number of molecules involved in reactions.

ReactICS

ReactICS is a toolkit that allows for verification of Reaction Systems.

The toolkit consists of two separate modules implementing:

• Methods using binary decision diagrams (BDD) for storing and manipulating the state space of the verified system.
• Methods translating the verification problems into satisfiability modulo theories (SMT).

Name

The name ReactICS pays tribute to VerICS, a verification tool for real-time and multi-agent systems developed at the Institute of Computer Science, Polish Academy of Sciences (ICS PAS), under the leadership of Wojciech Penczek. While VerICS laid the foundation for model checking complex temporal and epistemic properties, ReactICS extends this into the domain of Reaction Systems.

Features

BDD Module:

• Model checking for (distributed) reaction systems and properties expressed in rsCTLK (CTL, CTLK)
• State-space/graph generation
• Bounded model checking for verification of existential rsCTLK properties (or falsification of universal properties)
• Works with context automata
  • Guards on transitions that can be imposed also on local states of RS

SMT Module:

• Bounded model checking for the existential fragment of rsLTL
• Reaction systems with concentrations
• Parameter/reaction synthesis and parameter optimisation
• Produces witnesses

Obtaining ReactICS

The source code of ReactICS is available on Codeberg.

Please see Using ReactICS for instructions on how to build and run ReactICS.