Algorithms and tool support for the synthesis of Boolean nets (Marta Pietkiewicz-Koutny)
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). Relatively simple examples of such real-life systems range from VLSI hardware GALS systems to systems of living cells within which biochemical reactions happen in synchronised pulses. One way of capturing the resulting intricate behaviours is to use ENL-systems or safe PNL-nets (Boolean nets with localities) where transitions are partitioned into disjoint groups within which execution is synchronous, and otherwise it proceeds asynchronously. Additional challenge in modelling computer systems is to consider their concurrent behaviour and using in their analysis a concurrent semantics specified by connection monoids, which are essential part of describing different classes of Petri net models.
Within the domain of rigorous system design, automated synthesis from behavioural specifications is an attractive and yet still underdeveloped approach of constructing computational systems. Synthesis procedures guarantee that the resulting systems are correct, and so the time consuming process of system verification becomes redundant. The main problem in the area of automated synthesis is a lack of mature techniques and implemented tools capable of dealing with complex real-life system construction. In particular, there are no mature algorithms and implemented tools aimed at the synthesis of different kinds of Boolean nets from concurrent specifications. Addressing this issue is the overall goal of the proposed research project.
The proposed PhD project would concentrate on developing algorithms and building a tool that for a given behavioural description of a system (in the form of a step transition system) and a given specification of a class of Boolean nets (in the form of a net type) would assess whether the given behaviour can be realised as a Boolean net of the given type or not, and in the case of a positive answer would produce a net with the specified concurrent behaviour.