idDL2DL – interval syntax to dL

Abstract

A wide range of methods from computer science are being applied to many modern engineering domains, such as synthetic biology. Most behaviors described in synthetic biology have a hybrid nature, in the sense that both discrete or continuous dynamics are observed. Differential Dynamic Logic (dL) is a well-known formalism used for the rigorous treatment of these systems by considering formalisms comprising both differential equations and discrete assignments. Since the many systems often consider a range of values rather than exact values, due to errors and perturbations of observed quantities, recent work within the team proposed an interval version of dL, where variables are interpreted as intervals. This paper presents the first steps in the development of computational support for this formalism by introducing a tool designed to models based on intervals, prepared to translate them into specifications ready to be processed by the KeYmaera X tool.