Formal Semantics and Verification of Network Based Biocomputation Circuits
Network-Based Biocomputation Circuits (NBCs) offer a new paradigm for solving complex computational problems by utilizing biological agents that operate in parallel to explore manufactured planar devices. The approach can also have future applications in diagnostics and medicine by combining NBCs computational power with the ability to interface with biological material. To realize this potential, devices should be designed in a way that ensures their correctness and robust operation. For this purpose, formal methods and tools can offer significant advantages by allowing investigation of design limitations and detection of errors before manufacturing and experimentation. Here we define a computational model for NBCs by providing formal semantics to NBC circuits. We present a formal verification-based approach and prototype tool that can assist in the design of NBCs by enabling verification of a given design’s correctness. Our tool allows verification of the correctness of NBC designs for several NP-Complete problems, including the Subset Sum, Exact Cover and Satisfiability problems and can be extended to other NBC implementations. Our approach is based on defining transition systems for NBCs and using temporal logic for specifying and proving properties of the design using model checking. Our formal model can also serve as a starting point for computational complexity studies of the power and limitations of NBC systems.
Tue 19 Jan Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
18:00 - 18:30
|Formal Semantics and Verification of Network Based Biocomputation Circuits|
Michelle Aluf-MedinaBar Ilan University, Till KortenTU Dresden, Avraham RavivBar Ilan University, Dan Nicolau Jr.Molecular Sense, Hillel KuglerBar Ilan UniversityMedia Attached
|Netter: Probabilistic, Stateful Network Models|
Han ZhangCarnegie Mellon University, Chi Zhang, Arthur Azevedo de AmorimCarnegie Mellon University, USA, Yuvraj AgarwalCarnegie Mellon University, Matt FredriksonCarnegie Mellon University, Limin JiaCarnegie Mellon UniversityMedia Attached