Skip to content

Algorithms and tool support for the synthesis of Boolean nets

Boolean nets are a family of Petri net models capable of describing a great range of computational systems, such as VLSI hardware systems or biologically motivated membrane systems or reaction systems. Recently there is a growing interest in the modelling of systems whose behaviour combines synchrony with asynchrony in a variety of complicated ways (in this case, synchrony is related to logical or physical closeness of system components, and asynchrony to the operation of distant or loosely connected subsystems).

This project will investigate generic ways of defining specialised temporal logics for different kinds of Boolean nets, aiming at the adaptation of the existing model checkers and the development of novel efficient model checking tools.

Supervisors: Marta Pietkiewicz-Koutny (Computer Science, Newcastle), Maciej Koutny (Computer Science, Newcastle), Barnaby Martin (Computer Science, Durham)